:: AFF_2 semantic presentation
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_PPAP means :
E1:
:: AFF_2:def 1
for b
1, b
2 being
Subset of a
1for b
3, b
4, b
5, b
6, b
7, b
8 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 in b
1 & b
4 in b
1 & b
5 in b
1 & b
6 in b
2 & b
7 in b
2 & b
8 in b
2 & b
3,b
7 // b
4,b
6 & b
4,b
8 // b
5,b
7 ) implies ( b
3,b
8 // b
5,b
6 ) );
end;
:: deftheorem E1 defines satisfying_PPAP AFF_2:def 1 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_PPAP iff for b
2, b
3 being
Subset of b
1for b
4, b
5, b
6, b
7, b
8, b
9 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 in b
2 & b
5 in b
2 & b
6 in b
2 & b
7 in b
3 & b
8 in b
3 & b
9 in b
3 & b
4,b
8 // b
5,b
7 & b
5,b
9 // b
6,b
8 ) implies ( b
4,b
9 // b
6,b
7 ) ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
Pappian means :
E2:
:: AFF_2:def 2
for b
1, b
2 being
Subset of a
1for b
3, b
4, b
5, b
6, b
7, b
8, b
9 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 in b
1 & b
3 in b
2 & b
4 in b
1 & b
5 in b
1 & b
6 in b
1 & b
7 in b
2 & b
8 in b
2 & b
9 in b
2 & b
4,b
8 // b
5,b
7 & b
5,b
9 // b
6,b
8 ) implies ( not b
1 <> b
2 or not b
3 <> b
4 or not b
3 <> b
7 or not b
3 <> b
5 or not b
3 <> b
8 or not b
3 <> b
6 or not b
3 <> b
9 or b
4,b
9 // b
6,b
7 ) );
end;
:: deftheorem E2 defines Pappian AFF_2:def 2 :
for b
1 being
AffinSpace holds
( b
1 is
Pappian iff for b
2, b
3 being
Subset of b
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 in b
2 & b
4 in b
3 & b
5 in b
2 & b
6 in b
2 & b
7 in b
2 & b
8 in b
3 & b
9 in b
3 & b
10 in b
3 & b
5,b
9 // b
6,b
8 & b
6,b
10 // b
7,b
9 ) implies ( not b
2 <> b
3 or not b
4 <> b
5 or not b
4 <> b
8 or not b
4 <> b
6 or not b
4 <> b
9 or not b
4 <> b
7 or not b
4 <> b
10 or b
5,b
10 // b
7,b
8 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_PAP_1 means :
E3:
:: AFF_2:def 3
for b
1, b
2 being
Subset of a
1for b
3, b
4, b
5, b
6, b
7, b
8, b
9 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 in b
1 & b
3 in b
2 & b
4 in b
1 & b
5 in b
1 & b
6 in b
1 & b
8 in b
2 & b
9 in b
2 & b
4,b
8 // b
5,b
7 & b
5,b
9 // b
6,b
8 & b
4,b
9 // b
6,b
7 ) implies ( not b
1 <> b
2 or not b
3 <> b
4 or not b
3 <> b
7 or not b
3 <> b
5 or not b
3 <> b
8 or not b
3 <> b
6 or not b
3 <> b
9 or not b
5 <> b
6 or b
7 in b
2 ) );
end;
:: deftheorem E3 defines satisfying_PAP_1 AFF_2:def 3 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_PAP_1 iff for b
2, b
3 being
Subset of b
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 in b
2 & b
4 in b
3 & b
5 in b
2 & b
6 in b
2 & b
7 in b
2 & b
9 in b
3 & b
10 in b
3 & b
5,b
9 // b
6,b
8 & b
6,b
10 // b
7,b
9 & b
5,b
10 // b
7,b
8 ) implies ( not b
2 <> b
3 or not b
4 <> b
5 or not b
4 <> b
8 or not b
4 <> b
6 or not b
4 <> b
9 or not b
4 <> b
7 or not b
4 <> b
10 or not b
6 <> b
7 or b
8 in b
3 ) ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
Desarguesian means :
E4:
:: AFF_2:def 4
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10 being
Element of a
1 holds
( ( b
4 in b
1 & b
4 in b
2 & b
4 in b
3 & b
5 in b
1 & b
8 in b
1 & b
6 in b
2 & b
9 in b
2 & b
7 in b
3 & b
10 in b
3 & b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 ) implies ( not b
4 <> b
5 or not b
4 <> b
6 or not b
4 <> b
7 or not b
1 <> b
2 or not b
1 <> b
3 or b
6,b
7 // b
9,b
10 ) );
end;
:: deftheorem E4 defines Desarguesian AFF_2:def 4 :
for b
1 being
AffinSpace holds
( b
1 is
Desarguesian iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11 being
Element of b
1 holds
( ( b
5 in b
2 & b
5 in b
3 & b
5 in b
4 & b
6 in b
2 & b
9 in b
2 & b
7 in b
3 & b
10 in b
3 & b
8 in b
4 & b
11 in b
4 & b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
6,b
7 // b
9,b
10 & b
6,b
8 // b
9,b
11 ) implies ( not b
5 <> b
6 or not b
5 <> b
7 or not b
5 <> b
8 or not b
2 <> b
3 or not b
2 <> b
4 or b
7,b
8 // b
10,b
11 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES_1 means :
E5:
:: AFF_2:def 5
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10 being
Element of a
1 holds
( ( b
4 in b
1 & b
4 in b
2 & b
5 in b
1 & b
8 in b
1 & b
6 in b
2 & b
9 in b
2 & b
7 in b
3 & b
10 in b
3 & b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 & b
6,b
7 // b
9,b
10 ) implies ( not b
4 <> b
5 or not b
4 <> b
6 or not b
4 <> b
7 or not b
1 <> b
2 or not b
1 <> b
3 or
LIN b
5,b
6,b
7 or not b
7 <> b
10 or b
4 in b
3 ) );
end;
:: deftheorem E5 defines satisfying_DES_1 AFF_2:def 5 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES_1 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11 being
Element of b
1 holds
( ( b
5 in b
2 & b
5 in b
3 & b
6 in b
2 & b
9 in b
2 & b
7 in b
3 & b
10 in b
3 & b
8 in b
4 & b
11 in b
4 & b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
6,b
7 // b
9,b
10 & b
6,b
8 // b
9,b
11 & b
7,b
8 // b
10,b
11 ) implies ( not b
5 <> b
6 or not b
5 <> b
7 or not b
5 <> b
8 or not b
2 <> b
3 or not b
2 <> b
4 or
LIN b
6,b
7,b
8 or not b
8 <> b
11 or b
5 in b
4 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES_2 means :: AFF_2:def 6
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10 being
Element of a
1 holds
( ( b
4 in b
1 & b
4 in b
2 & b
4 in b
3 & b
5 in b
1 & b
8 in b
1 & b
6 in b
2 & b
9 in b
2 & b
7 in b
3 & b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 & b
6,b
7 // b
9,b
10 ) implies ( not b
4 <> b
5 or not b
4 <> b
6 or not b
4 <> b
7 or not b
1 <> b
2 or not b
1 <> b
3 or b
10 in b
3 ) );
end;
:: deftheorem defines satisfying_DES_2 AFF_2:def 6 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES_2 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11 being
Element of b
1 holds
( ( b
5 in b
2 & b
5 in b
3 & b
5 in b
4 & b
6 in b
2 & b
9 in b
2 & b
7 in b
3 & b
10 in b
3 & b
8 in b
4 & b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
6,b
7 // b
9,b
10 & b
6,b
8 // b
9,b
11 & b
7,b
8 // b
10,b
11 ) implies ( not b
5 <> b
6 or not b
5 <> b
7 or not b
5 <> b
8 or not b
2 <> b
3 or not b
2 <> b
4 or b
11 in b
4 ) ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
Moufangian means :
E6:
:: AFF_2:def 7
for b
1 being
Subset of a
1for b
2, b
3, b
4, b
5, b
6, b
7, b
8 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 in b
1 & b
5 in b
1 & b
8 in b
1 &
LIN b
2,b
3,b
6 &
LIN b
2,b
4,b
7 & b
3,b
4 // b
6,b
7 & b
3,b
5 // b
6,b
8 & b
3,b
4 // b
1 ) implies ( b
3 in b
1 or not b
2 <> b
5 or not b
3 <> b
4 or b
4,b
5 // b
7,b
8 ) );
end;
:: deftheorem E6 defines Moufangian AFF_2:def 7 :
for b
1 being
AffinSpace holds
( b
1 is
Moufangian iff for b
2 being
Subset of b
1for b
3, b
4, b
5, b
6, b
7, b
8, b
9 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 in b
2 & b
6 in b
2 & b
9 in b
2 &
LIN b
3,b
4,b
7 &
LIN b
3,b
5,b
8 & b
4,b
5 // b
7,b
8 & b
4,b
6 // b
7,b
9 & b
4,b
5 // b
2 ) implies ( b
4 in b
2 or not b
3 <> b
6 or not b
4 <> b
5 or b
5,b
6 // b
8,b
9 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_TDES_1 means :
E7:
:: AFF_2:def 8
for b
1 being
Subset of a
1for b
2, b
3, b
4, b
5, b
6, b
7, b
8 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 in b
1 & b
5 in b
1 & b
8 in b
1 &
LIN b
2,b
3,b
6 & b
3,b
4 // b
6,b
7 & b
4,b
5 // b
7,b
8 & b
3,b
5 // b
6,b
8 & b
3,b
4 // b
1 ) implies ( b
3 in b
1 or not b
2 <> b
5 or not b
3 <> b
4 or
LIN b
2,b
4,b
7 ) );
end;
:: deftheorem E7 defines satisfying_TDES_1 AFF_2:def 8 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_TDES_1 iff for b
2 being
Subset of b
1for b
3, b
4, b
5, b
6, b
7, b
8, b
9 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 in b
2 & b
6 in b
2 & b
9 in b
2 &
LIN b
3,b
4,b
7 & b
4,b
5 // b
7,b
8 & b
5,b
6 // b
8,b
9 & b
4,b
6 // b
7,b
9 & b
4,b
5 // b
2 ) implies ( b
4 in b
2 or not b
3 <> b
6 or not b
4 <> b
5 or
LIN b
3,b
5,b
8 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_TDES_2 means :
E8:
:: AFF_2:def 9
for b
1 being
Subset of a
1for b
2, b
3, b
4, b
5, b
6, b
7, b
8 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 in b
1 & b
5 in b
1 & b
8 in b
1 &
LIN b
2,b
3,b
6 &
LIN b
2,b
4,b
7 & b
4,b
5 // b
7,b
8 & b
3,b
5 // b
6,b
8 & b
3,b
4 // b
1 ) implies ( b
3 in b
1 or not b
2 <> b
5 or not b
3 <> b
4 or b
3,b
4 // b
6,b
7 ) );
end;
:: deftheorem E8 defines satisfying_TDES_2 AFF_2:def 9 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_TDES_2 iff for b
2 being
Subset of b
1for b
3, b
4, b
5, b
6, b
7, b
8, b
9 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 in b
2 & b
6 in b
2 & b
9 in b
2 &
LIN b
3,b
4,b
7 &
LIN b
3,b
5,b
8 & b
5,b
6 // b
8,b
9 & b
4,b
6 // b
7,b
9 & b
4,b
5 // b
2 ) implies ( b
4 in b
2 or not b
3 <> b
6 or not b
4 <> b
5 or b
4,b
5 // b
7,b
8 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_TDES_3 means :
E9:
:: AFF_2:def 10
for b
1 being
Subset of a
1for b
2, b
3, b
4, b
5, b
6, b
7, b
8 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 in b
1 & b
5 in b
1 &
LIN b
2,b
3,b
6 &
LIN b
2,b
4,b
7 & b
3,b
4 // b
6,b
7 & b
3,b
5 // b
6,b
8 & b
4,b
5 // b
7,b
8 & b
3,b
4 // b
1 ) implies ( b
3 in b
1 or not b
2 <> b
5 or not b
3 <> b
4 or b
8 in b
1 ) );
end;
:: deftheorem E9 defines satisfying_TDES_3 AFF_2:def 10 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_TDES_3 iff for b
2 being
Subset of b
1for b
3, b
4, b
5, b
6, b
7, b
8, b
9 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 in b
2 & b
6 in b
2 &
LIN b
3,b
4,b
7 &
LIN b
3,b
5,b
8 & b
4,b
5 // b
7,b
8 & b
4,b
6 // b
7,b
9 & b
5,b
6 // b
8,b
9 & b
4,b
5 // b
2 ) implies ( b
4 in b
2 or not b
3 <> b
6 or not b
4 <> b
5 or b
9 in b
2 ) ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
translational means :
E10:
:: AFF_2:def 11
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9 being
Element of a
1 holds
( ( b
1 // b
2 & b
1 // b
3 & b
4 in b
1 & b
7 in b
1 & b
5 in b
2 & b
8 in b
2 & b
6 in b
3 & b
9 in b
3 & b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4,b
5 // b
7,b
8 & b
4,b
6 // b
7,b
9 ) implies ( not b
1 <> b
2 or not b
1 <> b
3 or b
5,b
6 // b
8,b
9 ) );
end;
:: deftheorem E10 defines translational AFF_2:def 11 :
for b
1 being
AffinSpace holds
( b
1 is
translational iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10 being
Element of b
1 holds
( ( b
2 // b
3 & b
2 // b
4 & b
5 in b
2 & b
8 in b
2 & b
6 in b
3 & b
9 in b
3 & b
7 in b
4 & b
10 in b
4 & b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 ) implies ( not b
2 <> b
3 or not b
2 <> b
4 or b
6,b
7 // b
9,b
10 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_des_1 means :
E11:
:: AFF_2:def 12
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9 being
Element of a
1 holds
( ( b
1 // b
2 & b
4 in b
1 & b
7 in b
1 & b
5 in b
2 & b
8 in b
2 & b
6 in b
3 & b
9 in b
3 & b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4,b
5 // b
7,b
8 & b
4,b
6 // b
7,b
9 & b
5,b
6 // b
8,b
9 ) implies ( not b
1 <> b
2 or not b
1 <> b
3 or
LIN b
4,b
5,b
6 or not b
6 <> b
9 or b
1 // b
3 ) );
end;
:: deftheorem E11 defines satisfying_des_1 AFF_2:def 12 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_des_1 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10 being
Element of b
1 holds
( ( b
2 // b
3 & b
5 in b
2 & b
8 in b
2 & b
6 in b
3 & b
9 in b
3 & b
7 in b
4 & b
10 in b
4 & b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 & b
6,b
7 // b
9,b
10 ) implies ( not b
2 <> b
3 or not b
2 <> b
4 or
LIN b
5,b
6,b
7 or not b
7 <> b
10 or b
2 // b
4 ) ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
satisfying_pap means :
E12:
:: AFF_2:def 13
for b
1, b
2 being
Subset of a
1for b
3, b
4, b
5, b
6, b
7, b
8 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 in b
1 & b
4 in b
1 & b
5 in b
1 & b
1 // b
2 & b
6 in b
2 & b
7 in b
2 & b
8 in b
2 & b
3,b
7 // b
4,b
6 & b
4,b
8 // b
5,b
7 ) implies ( not b
1 <> b
2 or b
3,b
8 // b
5,b
6 ) );
end;
:: deftheorem E12 defines satisfying_pap AFF_2:def 13 :
for b
1 being
AffinSpace holds
( b
1 is
satisfying_pap iff for b
2, b
3 being
Subset of b
1for b
4, b
5, b
6, b
7, b
8, b
9 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 in b
2 & b
5 in b
2 & b
6 in b
2 & b
2 // b
3 & b
7 in b
3 & b
8 in b
3 & b
9 in b
3 & b
4,b
8 // b
5,b
7 & b
5,b
9 // b
6,b
8 ) implies ( not b
2 <> b
3 or b
4,b
9 // b
6,b
7 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_pap_1 means :
E13:
:: AFF_2:def 14
for b
1, b
2 being
Subset of a
1for b
3, b
4, b
5, b
6, b
7, b
8 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 in b
1 & b
4 in b
1 & b
5 in b
1 & b
1 // b
2 & b
6 in b
2 & b
7 in b
2 & b
3,b
7 // b
4,b
6 & b
4,b
8 // b
5,b
7 & b
3,b
8 // b
5,b
6 ) implies ( not b
1 <> b
2 or not b
6 <> b
7 or b
8 in b
2 ) );
end;
:: deftheorem E13 defines satisfying_pap_1 AFF_2:def 14 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_pap_1 iff for b
2, b
3 being
Subset of b
1for b
4, b
5, b
6, b
7, b
8, b
9 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 in b
2 & b
5 in b
2 & b
6 in b
2 & b
2 // b
3 & b
7 in b
3 & b
8 in b
3 & b
4,b
8 // b
5,b
7 & b
5,b
9 // b
6,b
8 & b
4,b
9 // b
6,b
7 ) implies ( not b
2 <> b
3 or not b
7 <> b
8 or b
9 in b
3 ) ) );
theorem :: AFF_2:1
canceled;
theorem :: AFF_2:2
canceled;
theorem :: AFF_2:3
canceled;
theorem :: AFF_2:4
canceled;
theorem :: AFF_2:5
canceled;
theorem :: AFF_2:6
canceled;
theorem :: AFF_2:7
canceled;
theorem :: AFF_2:8
canceled;
theorem :: AFF_2:9
canceled;
theorem :: AFF_2:10
canceled;
theorem :: AFF_2:11
canceled;
theorem :: AFF_2:12
canceled;
theorem :: AFF_2:13
canceled;
theorem :: AFF_2:14
canceled;
theorem :: AFF_2:15
proof
let c
1 be
AffinPlane;
E14:
now
assume E15:
c
1 is
satisfies_PAP
;
thus
c
1 is
satisfies_PAP_1
proof
let c
2 be
Subset of c
1;
:: uses AFF_2:def 3let c
3 be
Subset of c
1;
let c
4, c
5, c
6, c
7, c
8, c
9, c
10 be
Element of c
1;
assume E16:
( c
2 is
is_line & c
3 is
is_line & c
2 <> c
3 & c
4 in c
2 & c
4 in c
3 & c
4 <> c
5 & c
4 <> c
8 & c
4 <> c
6 & c
4 <> c
9 & c
4 <> c
7 & c
4 <> c
10 & c
5 in c
2 & c
6 in c
2 & c
7 in c
2 & c
9 in c
3 & c
10 in c
3 & c
5,c
9 // c
6,c
8 & c
6,c
10 // c
7,c
9 & c
5,c
10 // c
7,c
8 & c
6 <> c
7 )
;
assume E17:
not c
8 in c
3
;
E18:
( c
5 <> c
9 & c
5 <> c
10 )
by E16, AFF_1:30;
E19:
c
6 <> c
8
not c
6,c
8 // c
3
proof
assume
c
6,c
8 // c
3
;
then
( c
6,c
8 // c
3 & c
6,c
8 // c
5,c
9 )
by E16, AFF_1:13;
then
c
5,c
9 // c
3
by E19, AFF_1:46;
then
c
9,c
5 // c
3
by AFF_1:48;
then
c
5 in c
3
by E16, AFF_1:37;
hence
not verum
by E16, AFF_1:30;
end;
then consider c
11 being
Element of c
1 such that
E20:
( c
11 in c
3 &
LIN c
6,c
8,c
11 )
by E16, AFF_1:73;
E21:
c
5,c
9 // c
6,c
11
E22:
c
4 <> c
11
then
c
5,c
10 // c
7,c
11
by E15, E16, E20, E21, E2;
then
c
7,c
8 // c
7,c
11
by E16, E18, AFF_1:14;
then
LIN c
7,c
8,c
11
by AFF_1:def 1;
then
(
LIN c
8,c
11,c
7 &
LIN c
8,c
11,c
6 &
LIN c
8,c
11,c
11 )
by E20, AFF_1:15, AFF_1:16;
then
LIN c
6,c
7,c
11
by E17, E20, AFF_1:17;
then
c
11 in c
2
by E16, AFF_1:39;
hence
not verum
by E16, E20, E22, AFF_1:30;
end;
end;
now
assume E15:
c
1 is
satisfies_PAP_1
;
thus
c
1 is
satisfies_PAP
proof
let c
2 be
Subset of c
1;
:: uses AFF_2:def 2let c
3 be
Subset of c
1;
let c
4, c
5, c
6, c
7, c
8, c
9, c
10 be
Element of c
1;
assume E16:
( c
2 is
is_line & c
3 is
is_line & c
2 <> c
3 & c
4 in c
2 & c
4 in c
3 & c
4 <> c
5 & c
4 <> c
8 & c
4 <> c
6 & c
4 <> c
9 & c
4 <> c
7 & c
4 <> c
10 & c
5 in c
2 & c
6 in c
2 & c
7 in c
2 & c
8 in c
3 & c
9 in c
3 & c
10 in c
3 & c
5,c
9 // c
6,c
8 & c
6,c
10 // c
7,c
9 )
;
assume E17:
not c
5,c
10 // c
7,c
8
;
then E18:
( c
5 <> c
10 & c
7 <> c
8 )
by AFF_1:12;
E19:
( c
5 <> c
9 & c
6 <> c
8 )
by E16, AFF_1:30;
E20:
c
6 <> c
7
E21:
c
9 <> c
10
proof
assume
c
9 = c
10
;
then
c
9,c
6 // c
9,c
7
by E16, AFF_1:13;
then
LIN c
9,c
6,c
7
by AFF_1:def 1;
then
LIN c
6,c
7,c
9
by AFF_1:15;
then
c
9 in c
2
by E16, E20, AFF_1:39;
hence
not verum
by E16, AFF_1:30;
end;
set c
11 =
Line c
5,c
10;
set c
12 =
Line c
6,c
8;
E22:
(
Line c
5,c
10 is
is_line &
Line c
6,c
8 is
is_line & c
5 in Line c
5,c
10 & c
10 in Line c
5,c
10 & c
6 in Line c
6,c
8 & c
8 in Line c
6,c
8 )
by E18, E19, AFF_1:38;
then consider c
13 being
Subset of c
1 such that
E23:
( c
7 in c
13 &
Line c
5,c
10 // c
13 )
by AFF_1:63;
E24:
( c
13 is
is_line & c
13 // Line c
5,c
10 )
by E23, AFF_1:50;
not
Line c
6,c
8 // c
13
proof
assume
Line c
6,c
8 // c
13
;
then
Line c
6,c
8 // Line c
5,c
10
by E23, AFF_1:58;
then
c
6,c
8 // c
5,c
10
by E22, AFF_1:53;
then
c
5,c
9 // c
5,c
10
by E16, E19, AFF_1:14;
then
LIN c
5,c
9,c
10
by AFF_1:def 1;
then
LIN c
9,c
10,c
5
by AFF_1:15;
then
c
5 in c
3
by E16, E21, AFF_1:39;
hence
not verum
by E16, AFF_1:30;
end;
then consider c
14 being
Element of c
1 such that
E25:
( c
14 in Line c
6,c
8 & c
14 in c
13 )
by E22, E24, AFF_1:72;
E26:
c
5,c
10 // c
7,c
14
by E22, E23, E25, AFF_1:53;
c
5,c
9 // c
6,c
14
proof
LIN c
6,c
14,c
8
by E22, E25, AFF_1:33;
then
c
6,c
14 // c
6,c
8
by AFF_1:def 1;
hence
c
5,c
9 // c
6,c
14
by E16, E19, AFF_1:14;
end;
then
c
14 in c
3
by E15, E16, E20, E26, E3;
then
c
3 = Line c
6,c
8
by E16, E17, E22, E25, E26, AFF_1:30;
hence
not verum
by E16, E22, AFF_1:30;
end;
end;
hence
( c
1 is
satisfies_PAP iff c
1 is
satisfies_PAP_1 )
by E14;
end;
theorem :: AFF_2:16
proof
let c
1 be
AffinPlane;
E14:
now
assume E15:
c
1 is
satisfies_DES
;
thus
c
1 is
satisfies_DES_1
proof
let c
2 be
Subset of c
1;
:: uses AFF_2:def 5let c
3, c
4 be
Subset of c
1;
let c
5, c
6, c
7, c
8, c
9, c
10, c
11 be
Element of c
1;
assume E16:
( c
5 in c
2 & c
5 in c
3 & c
5 <> c
6 & c
5 <> c
7 & c
5 <> c
8 & c
6 in c
2 & c
9 in c
2 & c
7 in c
3 & c
10 in c
3 & c
8 in c
4 & c
11 in c
4 & c
2 is
is_line & c
3 is
is_line & c
4 is
is_line & c
2 <> c
3 & c
2 <> c
4 & c
6,c
7 // c
9,c
10 & c
6,c
8 // c
9,c
11 & c
7,c
8 // c
10,c
11 & not
LIN c
6,c
7,c
8 & c
8 <> c
11 )
;
assume E17:
not c
5 in c
4
;
set c
12 =
Line c
5,c
11;
E18:
(
Line c
5,c
11 is
is_line & c
5 in Line c
5,c
11 & c
11 in Line c
5,c
11 )
by E16, E17, AFF_1:38;
E19:
( c
6 <> c
7 & c
6 <> c
8 & c
7 <> c
8 )
by E16, AFF_1:16;
E20:
c
9 <> c
11
proof
assume E21:
c
9 = c
11
;
then
c
7,c
8 // c
9,c
10
by E16, AFF_1:13;
then
( c
6,c
7 // c
7,c
8 or c
9 = c
10 )
by E16, AFF_1:14;
then
( c
7,c
6 // c
7,c
8 or c
9 = c
10 )
by AFF_1:13;
then
(
LIN c
7,c
6,c
8 or c
9 = c
10 )
by AFF_1:def 1;
hence
not verum
by E16, E17, E21, AFF_1:15, AFF_1:30;
end;
E21:
c
10 <> c
11
proof
assume
c
10 = c
11
;
then
( c
9 = c
10 or c
6,c
8 // c
6,c
7 )
by E16, AFF_1:14;
then
( c
9 = c
10 or
LIN c
6,c
8,c
7 )
by AFF_1:def 1;
then
c
7,c
8 // c
6,c
8
by E16, E20, AFF_1:14, AFF_1:15;
then
c
8,c
7 // c
8,c
6
by AFF_1:13;
then
LIN c
8,c
7,c
6
by AFF_1:def 1;
hence
not verum
by E16, AFF_1:15;
end;
E22:
c
2 <> Line c
5,c
11
not c
6,c
8 // Line c
5,c
11
proof
assume
c
6,c
8 // Line c
5,c
11
;
then
c
9,c
11 // Line c
5,c
11
by E16, E19, AFF_1:46;
then
c
11,c
9 // Line c
5,c
11
by AFF_1:48;
then
c
9 in Line c
5,c
11
by E18, AFF_1:37;
then E23:
c
9 in c
3
by E16, E18, E22, AFF_1:30;
c
9,c
10 // c
7,c
6
by E16, AFF_1:13;
then
( c
9 = c
10 or c
6 in c
3 )
by E16, E23, AFF_1:62;
then
c
6,c
8 // c
7,c
8
by E16, E20, AFF_1:14, AFF_1:30;
then
c
8,c
6 // c
8,c
7
by AFF_1:13;
then
LIN c
8,c
6,c
7
by AFF_1:def 1;
hence
not verum
by E16, AFF_1:15;
end;
then consider c
13 being
Element of c
1 such that
E23:
( c
13 in Line c
5,c
11 &
LIN c
6,c
8,c
13 )
by E18, AFF_1:73;
E24:
c
6,c
8 // c
6,c
13
by E23, AFF_1:def 1;
then E25:
c
6,c
13 // c
9,c
11
by E16, E19, AFF_1:14;
E26:
not
LIN c
6,c
7,c
13
proof
assume
LIN c
6,c
7,c
13
;
then
c
6,c
7 // c
6,c
13
by AFF_1:def 1;
then
( c
6,c
7 // c
6,c
8 or c
6 = c
13 )
by E24, AFF_1:14;
hence
not verum
by E16, E18, E22, E23, AFF_1:30, AFF_1:def 1;
end;
c
5 <> c
13
then
c
7,c
13 // c
10,c
11
by E15, E16, E18, E22, E23, E25, E4;
then
( c
7,c
13 // c
7,c
8 &
LIN c
6,c
13,c
8 )
by E16, E21, E23, AFF_1:14, AFF_1:15;
then
c
8 in Line c
5,c
11
by E23, E26, AFF_1:23;
hence
not verum
by E16, E17, E18, AFF_1:30;
end;
end;
now
assume E15:
c
1 is
satisfies_DES_1
;
thus
c
1 is
satisfies_DES
proof
let c
2 be
Subset of c
1;
:: uses AFF_2:def 4let c
3, c
4 be
Subset of c
1;
let c
5, c
6, c
7, c
8, c
9, c
10, c
11 be
Element of c
1;
assume E16:
( c
5 in c
2 & c
5 in c
3 & c
5 in c
4 & c
5 <> c
6 & c
5 <> c
7 & c
5 <> c
8 & c
6 in c
2 & c
9 in c
2 & c
7 in c
3 & c
10 in c
3 & c
8 in c
4 & c
11 in c
4 & c
2 is
is_line & c
3 is
is_line & c
4 is
is_line & c
2 <> c
3 & c
2 <> c
4 & c
6,c
7 // c
9,c
10 & c
6,c
8 // c
9,c
11 )
;
assume E17:
not c
7,c
8 // c
10,c
11
;
then E18:
( c
7 <> c
8 & c
10 <> c
11 )
by AFF_1:12;
E19:
c
6 <> c
7
by E16, AFF_1:30;
E20:
c
6 <> c
8
by E16, AFF_1:30;
E21:
c
9 <> c
10
E22:
c
9 <> c
11
E23:
not
LIN c
9,c
10,c
11
proof
assume
LIN c
9,c
10,c
11
;
then
( c
9,c
10 // c
9,c
11 &
LIN c
10,c
11,c
9 )
by AFF_1:15, AFF_1:def 1;
then E24:
( c
9,c
10 // c
6,c
8 & c
10,c
11 // c
10,c
9 )
by E16, E22, AFF_1:14, AFF_1:def 1;
then
c
6,c
7 // c
6,c
8
by E16, E21, AFF_1:14;
then
LIN c
6,c
7,c
8
by AFF_1:def 1;
then
LIN c
7,c
8,c
6
by AFF_1:15;
then
c
7,c
8 // c
7,c
6
by AFF_1:def 1;
then
c
7,c
8 // c
6,c
7
by AFF_1:13;
then
( c
7,c
8 // c
9,c
10 & c
10,c
11 // c
9,c
10 )
by E16, E19, E24, AFF_1:13, AFF_1:14;
hence
not verum
by E17, E21, AFF_1:14;
end;
E24:
c
6 <> c
9
proof
assume
c
6 = c
9
;
then
(
LIN c
6,c
7,c
10 &
LIN c
6,c
8,c
11 )
by E16, AFF_1:def 1;
then
(
LIN c
7,c
10,c
6 &
LIN c
8,c
11,c
6 )
by AFF_1:15;
then
( ( c
7 = c
10 or c
6 in c
3 ) & ( c
8 = c
11 or c
6 in c
4 ) )
by E16, AFF_1:39;
hence
not verum
by E16, E17, AFF_1:11, AFF_1:30;
end;
E25:
c
5 <> c
11
set c
12 =
Line c
9,c
11;
set c
13 =
Line c
6,c
8;
set c
14 =
Line c
10,c
11;
E26:
(
Line c
9,c
11 is
is_line &
Line c
6,c
8 is
is_line &
Line c
10,c
11 is
is_line & c
9 in Line c
9,c
11 & c
11 in Line c
9,c
11 & c
6 in Line c
6,c
8 & c
8 in Line c
6,c
8 & c
10 in Line c
10,c
11 & c
11 in Line c
10,c
11 )
by E18, E20, E22, AFF_1:38;
then consider c
15 being
Subset of c
1 such that
E27:
( c
7 in c
15 &
Line c
10,c
11 // c
15 )
by AFF_1:63;
E28:
( c
15 is
is_line & c
15 // Line c
10,c
11 )
by E27, AFF_1:50;
not
Line c
6,c
8 // c
15
proof
assume
Line c
6,c
8 // c
15
;
then
Line c
6,c
8 // Line c
10,c
11
by E27, AFF_1:58;
then
c
6,c
8 // c
10,c
11
by E26, AFF_1:53;
then
c
9,c
11 // c
10,c
11
by E16, E20, AFF_1:14;
then
c
11,c
9 // c
11,c
10
by AFF_1:13;
then
LIN c
11,c
9,c
10
by AFF_1:def 1;
hence
not verum
by E23, AFF_1:15;
end;
then consider c
16 being
Element of c
1 such that
E29:
( c
16 in Line c
6,c
8 & c
16 in c
15 )
by E26, E28, AFF_1:72;
E30:
c
6,c
16 // c
9,c
11
proof
LIN c
6,c
8,c
16
by E26, E29, AFF_1:33;
then
c
6,c
8 // c
6,c
16
by AFF_1:def 1;
hence
c
6,c
16 // c
9,c
11
by E16, E20, AFF_1:14;
end;
E31:
c
7,c
16 // c
10,c
11
by E26, E27, E29, AFF_1:53;
E32:
c
16 <> c
11
proof
assume
c
16 = c
11
;
then
c
11,c
6 // c
11,c
9
by E30, AFF_1:13;
then
LIN c
11,c
6,c
9
by AFF_1:def 1;
then
LIN c
6,c
9,c
11
by AFF_1:15;
then
c
11 in c
2
by E16, E24, AFF_1:39;
hence
not verum
by E16, E25, AFF_1:30;
end;
E33:
c
6 <> c
16
proof
assume
c
6 = c
16
;
then
c
6,c
7 // c
10,c
11
by E26, E27, E29, AFF_1:53;
then
c
9,c
10 // c
10,c
11
by E16, E19, AFF_1:14;
then
c
10,c
9 // c
10,c
11
by AFF_1:13;
then
LIN c
10,c
9,c
11
by AFF_1:def 1;
hence
not verum
by E23, AFF_1:15;
end;
E34:
not
LIN c
6,c
7,c
16
proof
assume
LIN c
6,c
7,c
16
;
then
c
6,c
7 // c
6,c
16
by AFF_1:def 1;
then
c
6,c
7 // c
9,c
11
by E30, E33, AFF_1:14;
then
c
9,c
10 // c
9,c
11
by E16, E19, AFF_1:14;
hence
not verum
by E23, AFF_1:def 1;
end;
set c
17 =
Line c
11,c
16;
E35:
(
Line c
11,c
16 is
is_line & c
11 in Line c
11,c
16 & c
16 in Line c
11,c
16 )
by E32, AFF_1:38;
then
c
5 in Line c
11,c
16
by E15, E16, E30, E31, E32, E34, E5;
then
c
16 in c
4
by E16, E25, E35, AFF_1:30;
then
c
4 = Line c
6,c
8
by E16, E17, E26, E29, E31, AFF_1:30;
hence
not verum
by E16, E26, AFF_1:30;
end;
end;
hence
( c
1 is
satisfies_DES iff c
1 is
satisfies_DES_1 )
by E14;
end;
theorem E14: :: AFF_2:17
proof
let c
1 be
AffinPlane;
assume E15:
c
1 is
satisfies_TDES
;
thus
c
1 is
satisfies_TDES_1
proof
let c
2 be
Subset of c
1;
:: uses AFF_2:def 8let c
3, c
4, c
5, c
6, c
7, c
8, c
9 be
Element of c
1;
assume that
E16:
c
2 is
is_line
and
E17:
( c
3 in c
2 & c
6 in c
2 & c
9 in c
2 )
and
E18:
not c
4 in c
2
and
E19:
( c
3 <> c
6 & c
4 <> c
5 &
LIN c
3,c
4,c
7 & c
4,c
5 // c
7,c
8 & c
5,c
6 // c
8,c
9 & c
4,c
6 // c
7,c
9 & c
4,c
5 // c
2 )
;
assume E20:
not
LIN c
3,c
5,c
8
;
E21:
not c
5 in c
2
by E18, E19, AFF_1:49;
E22:
c
5 <> c
6
by E17, E18, E19, AFF_1:49;
E23:
( c
3 <> c
5 & c
3 <> c
4 )
by E17, E18, E20, AFF_1:16;
set c
10 =
Line c
3,c
5;
set c
11 =
Line c
3,c
4;
E24:
(
Line c
3,c
5 is
is_line &
Line c
3,c
4 is
is_line & c
3 in Line c
3,c
5 & c
5 in Line c
3,c
5 & c
3 in Line c
3,c
4 & c
4 in Line c
3,c
4 )
by E23, AFF_1:26, AFF_1:def 3;
then E25:
c
7 in Line c
3,c
4
by E17, E18, E19, AFF_1:39;
consider c
12 being
Subset of c
1 such that
E26:
( c
7 in c
12 & c
2 // c
12 )
by E16, AFF_1:63;
E27:
( c
12 is
is_line & c
12 // c
2 )
by E26, AFF_1:50;
not
Line c
3,c
5 // c
12
then consider c
13 being
Element of c
1 such that
E28:
( c
13 in Line c
3,c
5 & c
13 in c
12 )
by E24, E27, AFF_1:72;
E29:
LIN c
3,c
5,c
13
by E24, E28, AFF_1:33;
c
4,c
5 // c
7,c
13
then
c
5,c
6 // c
13,c
9
by E15, E16, E17, E18, E19, E29, E6;
then
c
8,c
9 // c
13,c
9
by E19, E22, AFF_1:14;
then
c
9,c
8 // c
9,c
13
by AFF_1:13;
then
LIN c
9,c
8,c
13
by AFF_1:def 1;
then E30:
LIN c
8,c
13,c
9
by AFF_1:15;
c
4,c
5 // c
12
by E19, E26, AFF_1:57;
then
c
7,c
8 // c
12
by E19, AFF_1:46;
then E31:
c
8 in c
12
by E26, E27, AFF_1:37;
then
(
LIN c
8,c
13,c
7 &
LIN c
8,c
13,c
8 )
by E26, E27, E28, AFF_1:33;
then
LIN c
8,c
9,c
7
by E20, E29, E30, AFF_1:17;
then
c
8,c
9 // c
8,c
7
by AFF_1:def 1;
then E32:
c
8,c
9 // c
7,c
8
by AFF_1:13;
E33:
c
8 <> c
9
proof
assume E34:
c
8 = c
9
;
then
c
12 = c
2
by E17, E26, E31, AFF_1:59;
then E35:
c
7 = c
3
by E16, E17, E18, E24, E25, E26, AFF_1:30;
c
7,c
9 // c
6,c
4
by E19, AFF_1:13;
then
c
8 = c
3
by E16, E17, E18, E34, E35, AFF_1:62;
hence
not verum
by E20, AFF_1:16;
end;
E34:
c
7 <> c
8
proof
assume E35:
c
7 = c
8
;
then E36:
( c
4,c
6 // c
5,c
6 or c
7 = c
9 )
by E19, AFF_1:14;
now
assume
c
7 = c
9
;
then
c
8 = c
3
by E16, E17, E18, E24, E25, E35, AFF_1:30;
hence
not verum
by E20, AFF_1:16;
end;
then
c
6,c
4 // c
6,c
5
by E36, AFF_1:13;
then
LIN c
6,c
4,c
5
by AFF_1:def 1;
then
LIN c
4,c
6,c
5
by AFF_1:15;
then
c
4,c
6 // c
4,c
5
by AFF_1:def 1;
then
c
4,c
5 // c
4,c
6
by AFF_1:13;
then
c
4,c
6 // c
2
by E19, AFF_1:46;
then
c
6,c
4 // c
2
by AFF_1:48;
hence
not verum
by E16, E17, E18, AFF_1:37;
end;
c
5,c
6 // c
7,c
8
by E19, E32, E33, AFF_1:14;
then
c
4,c
5 // c
5,c
6
by E19, E34, AFF_1:14;
then
c
5,c
6 // c
2
by E19, AFF_1:46;
then
c
6,c
5 // c
2
by AFF_1:48;
hence
not verum
by E16, E17, E21, AFF_1:37;
end;
end;
theorem :: AFF_2:18
proof
let c
1 be
AffinPlane;
assume E15:
c
1 is
satisfies_TDES_1
;
thus
c
1 is
satisfies_TDES_2
proof
let c
2 be
Subset of c
1;
:: uses AFF_2:def 9let c
3, c
4, c
5, c
6, c
7, c
8, c
9 be
Element of c
1;
assume E16:
( c
2 is
is_line & c
3 in c
2 & c
6 in c
2 & c
9 in c
2 & not c
4 in c
2 & c
3 <> c
6 & c
4 <> c
5 &
LIN c
3,c
4,c
7 &
LIN c
3,c
5,c
8 & c
5,c
6 // c
8,c
9 & c
4,c
6 // c
7,c
9 & c
4,c
5 // c
2 )
;
assume E17:
not c
4,c
5 // c
7,c
8
;
then E18:
c
7 <> c
8
by AFF_1:12;
E19:
not c
5 in c
2
by E16, AFF_1:49;
E20:
( c
3 <> c
4 & c
3 <> c
5 )
by E16, AFF_1:49;
set c
10 =
Line c
3,c
4;
set c
11 =
Line c
3,c
5;
E21:
(
Line c
3,c
4 is
is_line &
Line c
3,c
5 is
is_line & c
3 in Line c
3,c
4 & c
4 in Line c
3,c
4 & c
3 in Line c
3,c
5 & c
5 in Line c
3,c
5 )
by E20, AFF_1:38;
then E22:
( c
7 in Line c
3,c
4 & c
8 in Line c
3,c
5 )
by E16, E20, AFF_1:39;
E23:
not c
8 in c
2
proof
assume E24:
c
8 in c
2
;
then E25:
c
8 = c
3
by E16, E19, E21, E22, AFF_1:30;
E26:
c
8,c
9 // c
6,c
5
by E16, AFF_1:13;
then
( c
9 in Line c
3,c
4 & c
7,c
9 // c
4,c
6 )
by E16, E19, E21, E25, AFF_1:13, AFF_1:62;
then
( c
7 = c
9 or c
6 in Line c
3,c
4 )
by E21, E22, AFF_1:62;
hence
not verum
by E16, E18, E19, E21, E24, E26, AFF_1:30, AFF_1:62;
end;
set c
12 =
Line c
8,c
9;
E24:
(
Line c
8,c
9 is
is_line & c
8 in Line c
8,c
9 & c
9 in Line c
8,c
9 )
by E16, E23, AFF_1:38;
consider c
13 being
Subset of c
1 such that
E25:
( c
7 in c
13 & c
2 // c
13 )
by E16, AFF_1:63;
E26:
( c
13 is
is_line & c
13 // c
2 )
by E25, AFF_1:50;
not c
13 // Line c
8,c
9
then consider c
14 being
Element of c
1 such that
E27:
( c
14 in c
13 & c
14 in Line c
8,c
9 )
by E24, E26, AFF_1:72;
c
7,c
14 // c
2
by E25, E27, AFF_1:54;
then E28:
c
4,c
5 // c
7,c
14
by E16, AFF_1:45;
c
5,c
6 // c
14,c
9
proof
LIN c
9,c
8,c
14
by E24, E27, AFF_1:33;
then
c
9,c
8 // c
9,c
14
by AFF_1:def 1;
then
c
8,c
9 // c
14,c
9
by AFF_1:13;
hence
c
5,c
6 // c
14,c
9
by E16, E23, AFF_1:14;
end;
then
LIN c
3,c
5,c
14
by E15, E16