:: AFF_2 semantic presentation
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_PPAP means :
Def1:
:: 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_line & b
2 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 Def1 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_line & b
3 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 :
Def2:
:: 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_line & b
2 is_line & b
1 <> b
2 & b
3 in b
1 & b
3 in b
2 & b
3 <> b
4 & b
3 <> b
7 & b
3 <> b
5 & b
3 <> b
8 & b
3 <> b
6 & b
3 <> b
9 & 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 b
4,b
9 // b
6,b
7 );
end;
:: deftheorem Def2 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_line & b
3 is_line & b
2 <> b
3 & b
4 in b
2 & b
4 in b
3 & b
4 <> b
5 & b
4 <> b
8 & b
4 <> b
6 & b
4 <> b
9 & b
4 <> b
7 & b
4 <> b
10 & 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 b
5,b
10 // b
7,b
8 ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_PAP_1 means :
Def3:
:: 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_line & b
2 is_line & b
1 <> b
2 & b
3 in b
1 & b
3 in b
2 & b
3 <> b
4 & b
3 <> b
7 & b
3 <> b
5 & b
3 <> b
8 & b
3 <> b
6 & b
3 <> b
9 & 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 & b
5 <> b
6 implies b
7 in b
2 );
end;
:: deftheorem Def3 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_line & b
3 is_line & b
2 <> b
3 & b
4 in b
2 & b
4 in b
3 & b
4 <> b
5 & b
4 <> b
8 & b
4 <> b
6 & b
4 <> b
9 & b
4 <> b
7 & b
4 <> b
10 & 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 & b
6 <> b
7 implies b
8 in b
3 ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
Desarguesian means :
Def4:
:: 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
4 <> b
5 & b
4 <> b
6 & b
4 <> b
7 & 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_line & b
2 is_line & b
3 is_line & b
1 <> b
2 & b
1 <> b
3 & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 implies b
6,b
7 // b
9,b
10 );
end;
:: deftheorem Def4 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
5 <> b
6 & b
5 <> b
7 & b
5 <> b
8 & 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_line & b
3 is_line & b
4 is_line & b
2 <> b
3 & b
2 <> b
4 & b
6,b
7 // b
9,b
10 & b
6,b
8 // b
9,b
11 implies b
7,b
8 // b
10,b
11 ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES_1 means :
Def5:
:: 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
4 <> b
5 & b
4 <> b
6 & b
4 <> b
7 & 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_line & b
2 is_line & b
3 is_line & b
1 <> b
2 & b
1 <> b
3 & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 & b
6,b
7 // b
9,b
10 & not
LIN b
5,b
6,b
7 & b
7 <> b
10 implies b
4 in b
3 );
end;
:: deftheorem Def5 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
5 <> b
6 & b
5 <> b
7 & b
5 <> b
8 & 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_line & b
3 is_line & b
4 is_line & b
2 <> b
3 & b
2 <> b
4 & b
6,b
7 // b
9,b
10 & b
6,b
8 // b
9,b
11 & b
7,b
8 // b
10,b
11 & not
LIN b
6,b
7,b
8 & b
8 <> b
11 implies 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
4 <> b
5 & b
4 <> b
6 & b
4 <> b
7 & 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_line & b
2 is_line & b
3 is_line & b
1 <> b
2 & b
1 <> b
3 & 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 b
10 in b
3 );
end;
:: deftheorem Def6 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
5 <> b
6 & b
5 <> b
7 & b
5 <> b
8 & 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_line & b
3 is_line & b
4 is_line & b
2 <> b
3 & b
2 <> b
4 & 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 b
11 in b
4 ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
Moufangian means :
Def7:
:: 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_line & b
2 in b
1 & b
5 in b
1 & b
8 in b
1 & not b
3 in b
1 & b
2 <> b
5 & b
3 <> b
4 &
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
4,b
5 // b
7,b
8 );
end;
:: deftheorem Def7 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_line & b
3 in b
2 & b
6 in b
2 & b
9 in b
2 & not b
4 in b
2 & b
3 <> b
6 & b
4 <> b
5 &
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
5,b
6 // b
8,b
9 ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_TDES_1 means :
Def8:
:: 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_line & b
2 in b
1 & b
5 in b
1 & b
8 in b
1 & not b
3 in b
1 & b
2 <> b
5 & b
3 <> b
4 &
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
LIN b
2,b
4,b
7 );
end;
:: deftheorem Def8 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_line & b
3 in b
2 & b
6 in b
2 & b
9 in b
2 & not b
4 in b
2 & b
3 <> b
6 & b
4 <> b
5 &
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
LIN b
3,b
5,b
8 ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_TDES_2 means :
Def9:
:: 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_line & b
2 in b
1 & b
5 in b
1 & b
8 in b
1 & not b
3 in b
1 & b
2 <> b
5 & b
3 <> b
4 &
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,b
4 // b
6,b
7 );
end;
:: deftheorem Def9 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_line & b
3 in b
2 & b
6 in b
2 & b
9 in b
2 & not b
4 in b
2 & b
3 <> b
6 & b
4 <> b
5 &
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,b
5 // b
7,b
8 ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_TDES_3 means :
Def10:
:: 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_line & b
2 in b
1 & b
5 in b
1 & not b
3 in b
1 & b
2 <> b
5 & b
3 <> b
4 &
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
8 in b
1 );
end;
:: deftheorem Def10 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_line & b
3 in b
2 & b
6 in b
2 & not b
4 in b
2 & b
3 <> b
6 & b
4 <> b
5 &
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
9 in b
2 ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
translational means :
Def11:
:: 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_line & b
2 is_line & b
3 is_line & b
1 <> b
2 & b
1 <> b
3 & b
4,b
5 // b
7,b
8 & b
4,b
6 // b
7,b
9 implies b
5,b
6 // b
8,b
9 );
end;
:: deftheorem Def11 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_line & b
3 is_line & b
4 is_line & b
2 <> b
3 & b
2 <> b
4 & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 implies b
6,b
7 // b
9,b
10 ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_des_1 means :
Def12:
:: 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_line & b
2 is_line & b
3 is_line & b
1 <> b
2 & b
1 <> b
3 & b
4,b
5 // b
7,b
8 & b
4,b
6 // b
7,b
9 & b
5,b
6 // b
8,b
9 & not
LIN b
4,b
5,b
6 & b
6 <> b
9 implies b
1 // b
3 );
end;
:: deftheorem Def12 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_line & b
3 is_line & b
4 is_line & b
2 <> b
3 & b
2 <> b
4 & b
5,b
6 // b
8,b
9 & b
5,b
7 // b
8,b
10 & b
6,b
7 // b
9,b
10 & not
LIN b
5,b
6,b
7 & b
7 <> b
10 implies b
2 // b
4 ) );
definition
let c
1 be
AffinSpace;
attr a
1 is
satisfying_pap means :
Def13:
:: 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_line & b
2 is_line & b
3 in b
1 & b
4 in b
1 & b
5 in b
1 & b
1 // b
2 & 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 b
3,b
8 // b
5,b
6 );
end;
:: deftheorem Def13 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_line & b
3 is_line & b
4 in b
2 & b
5 in b
2 & b
6 in b
2 & b
2 // b
3 & 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 b
4,b
9 // b
6,b
7 ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_pap_1 means :
Def14:
:: 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_line & b
2 is_line & b
3 in b
1 & b
4 in b
1 & b
5 in b
1 & b
1 // b
2 & 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 & b
6 <> b
7 implies b
8 in b
2 );
end;
:: deftheorem Def14 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_line & b
3 is_line & b
4 in b
2 & b
5 in b
2 & b
6 in b
2 & b
2 // b
3 & 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 & b
7 <> b
8 implies b
9 in b
3 ) );
theorem Th1: :: AFF_2:1
canceled;
theorem Th2: :: AFF_2:2
canceled;
theorem Th3: :: AFF_2:3
canceled;
theorem Th4: :: AFF_2:4
canceled;
theorem Th5: :: AFF_2:5
canceled;
theorem Th6: :: AFF_2:6
canceled;
theorem Th7: :: AFF_2:7
canceled;
theorem Th8: :: AFF_2:8
canceled;
theorem Th9: :: AFF_2:9
canceled;
theorem Th10: :: AFF_2:10
canceled;
theorem Th11: :: AFF_2:11
canceled;
theorem Th12: :: AFF_2:12
canceled;
theorem Th13: :: AFF_2:13
canceled;
theorem Th14: :: AFF_2:14
canceled;
theorem Th15: :: AFF_2:15
proof
let c
1 be
AffinPlane;
E14:
now
assume E15:
c
1 satisfies_PAP
;
thus
c
1 satisfies_PAP_1
proof
let c
2 be
Subset of c
1;
:: according to 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_line & c
3 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, Def2;
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 satisfies_PAP_1
;
thus
c
1 satisfies_PAP
proof
let c
2 be
Subset of c
1;
:: according to 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_line & c
3 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_line &
Line c
6,c
8 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_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, Def3;
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 satisfies_PAP iff c
1 satisfies_PAP_1 )
by E14;
end;
theorem Th16: :: AFF_2:16
proof
let c
1 be
AffinPlane;
E14:
now
assume E15:
c
1 satisfies_DES
;
thus
c
1 satisfies_DES_1
proof
let c
2 be
Subset of c
1;
:: according to 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_line & c
3 is_line & c
4 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_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, Def4;
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 satisfies_DES_1
;
thus
c
1 satisfies_DES
proof
let c
2 be
Subset of c
1;
:: according to 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_line & c
3 is_line & c
4 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_line &
Line c
6,c
8 is_line &
Line c
10,c
11 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_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_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, Def5;
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,