:: AFF_2 semantic presentation
begin
definition
let AP be AffinPlane;
attrAP is satisfying_PPAP means :Def1: :: AFF_2:def 1
for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9;
end;
:: deftheorem Def1 defines satisfying_PPAP AFF_2:def_1_:_
for AP being AffinPlane holds
( AP is satisfying_PPAP iff for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9 );
definition
let AP be AffinSpace;
attrAP is Pappian means :Def2: :: AFF_2:def 2
for M, N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9;
end;
:: deftheorem Def2 defines Pappian AFF_2:def_2_:_
for AP being AffinSpace holds
( AP is Pappian iff for M, N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9 );
definition
let AP be AffinPlane;
attrAP is satisfying_PAP_1 means :Def3: :: AFF_2:def 3
for M, N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds
a9 in N;
end;
:: deftheorem Def3 defines satisfying_PAP_1 AFF_2:def_3_:_
for AP being AffinPlane holds
( AP is satisfying_PAP_1 iff for M, N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds
a9 in N );
definition
let AP be AffinSpace;
attrAP is Desarguesian means :Def4: :: AFF_2:def 4
for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9;
end;
:: deftheorem Def4 defines Desarguesian AFF_2:def_4_:_
for AP being AffinSpace holds
( AP is Desarguesian iff for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 );
definition
let AP be AffinPlane;
attrAP is satisfying_DES_1 means :Def5: :: AFF_2:def 5
for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
o in C;
end;
:: deftheorem Def5 defines satisfying_DES_1 AFF_2:def_5_:_
for AP being AffinPlane holds
( AP is satisfying_DES_1 iff for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
o in C );
definition
let AP be AffinPlane;
attrAP is satisfying_DES_2 means :: AFF_2:def 6
for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 holds
c9 in C;
end;
:: deftheorem defines satisfying_DES_2 AFF_2:def_6_:_
for AP being AffinPlane holds
( AP is satisfying_DES_2 iff for A, P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 holds
c9 in C );
definition
let AP be AffinSpace;
attrAP is Moufangian means :Def7: :: AFF_2:def 7
for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9;
end;
:: deftheorem Def7 defines Moufangian AFF_2:def_7_:_
for AP being AffinSpace holds
( AP is Moufangian iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9 );
definition
let AP be AffinPlane;
attrAP is satisfying_TDES_1 means :Def8: :: AFF_2:def 8
for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9;
end;
:: deftheorem Def8 defines satisfying_TDES_1 AFF_2:def_8_:_
for AP being AffinPlane holds
( AP is satisfying_TDES_1 iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9 );
definition
let AP be AffinPlane;
attrAP is satisfying_TDES_2 means :Def9: :: AFF_2:def 9
for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
a,b // a9,b9;
end;
:: deftheorem Def9 defines satisfying_TDES_2 AFF_2:def_9_:_
for AP being AffinPlane holds
( AP is satisfying_TDES_2 iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
a,b // a9,b9 );
definition
let AP be AffinPlane;
attrAP is satisfying_TDES_3 means :Def10: :: AFF_2:def 10
for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & a,b // K holds
c9 in K;
end;
:: deftheorem Def10 defines satisfying_TDES_3 AFF_2:def_10_:_
for AP being AffinPlane holds
( AP is satisfying_TDES_3 iff for K being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & a,b // K holds
c9 in K );
definition
let AP be AffinSpace;
attrAP is translational means :Def11: :: AFF_2:def 11
for A, P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9;
end;
:: deftheorem Def11 defines translational AFF_2:def_11_:_
for AP being AffinSpace holds
( AP is translational iff for A, P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 );
definition
let AP be AffinPlane;
attrAP is satisfying_des_1 means :Def12: :: AFF_2:def 12
for A, P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C;
end;
:: deftheorem Def12 defines satisfying_des_1 AFF_2:def_12_:_
for AP being AffinPlane holds
( AP is satisfying_des_1 iff for A, P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C );
definition
let AP be AffinSpace;
attrAP is satisfying_pap means :Def13: :: AFF_2:def 13
for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9;
end;
:: deftheorem Def13 defines satisfying_pap AFF_2:def_13_:_
for AP being AffinSpace holds
( AP is satisfying_pap iff for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9 );
definition
let AP be AffinPlane;
attrAP is satisfying_pap_1 means :Def14: :: AFF_2:def 14
for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds
c9 in N;
end;
:: deftheorem Def14 defines satisfying_pap_1 AFF_2:def_14_:_
for AP being AffinPlane holds
( AP is satisfying_pap_1 iff for M, N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds
c9 in N );
theorem :: AFF_2:1
for AP being AffinPlane holds
( AP is Pappian iff AP is satisfying_PAP_1 )
proof
let AP be AffinPlane; ::_thesis: ( AP is Pappian iff AP is satisfying_PAP_1 )
hereby ::_thesis: ( AP is satisfying_PAP_1 implies AP is Pappian )
assume A1: AP is Pappian ; ::_thesis: AP is satisfying_PAP_1
thus AP is satisfying_PAP_1 ::_thesis: verum
proof
let M be Subset of AP; :: according to AFF_2:def_3 ::_thesis: for N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds
a9 in N
let N be Subset of AP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c holds
a9 in N
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & b <> c implies a9 in N )
assume that
A2: M is being_line and
A3: N is being_line and
A4: M <> N and
A5: o in M and
A6: o in N and
A7: o <> a and
o <> a9 and
A8: o <> b and
A9: o <> b9 and
A10: o <> c and
A11: o <> c9 and
A12: a in M and
A13: b in M and
A14: c in M and
A15: b9 in N and
A16: c9 in N and
A17: a,b9 // b,a9 and
A18: b,c9 // c,b9 and
A19: a,c9 // c,a9 and
A20: b <> c ; ::_thesis: a9 in N
A21: a <> c9 by A2, A3, A4, A5, A6, A7, A12, A16, AFF_1:18;
A22: b <> a9
proof
assume b = a9 ; ::_thesis: contradiction
then c,b // a,c9 by A19, AFF_1:4;
then c9 in M by A2, A12, A13, A14, A20, AFF_1:48;
hence contradiction by A2, A3, A4, A5, A6, A11, A16, AFF_1:18; ::_thesis: verum
end;
not b,a9 // N
proof
assume A23: b,a9 // N ; ::_thesis: contradiction
b,a9 // a,b9 by A17, AFF_1:4;
then a,b9 // N by A22, A23, AFF_1:32;
then b9,a // N by AFF_1:34;
then a in N by A3, A15, AFF_1:23;
hence contradiction by A2, A3, A4, A5, A6, A7, A12, AFF_1:18; ::_thesis: verum
end;
then consider x being Element of AP such that
A24: x in N and
A25: LIN b,a9,x by A3, AFF_1:59;
A26: b,a9 // b,x by A25, AFF_1:def_1;
A27: o <> x
proof
assume o = x ; ::_thesis: contradiction
then b,o // a,b9 by A17, A22, A26, AFF_1:5;
then b9 in M by A2, A5, A8, A12, A13, AFF_1:48;
hence contradiction by A2, A3, A4, A5, A6, A9, A15, AFF_1:18; ::_thesis: verum
end;
a,b9 // b,x by A17, A22, A26, AFF_1:5;
then a,c9 // c,x by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A18, A24, A27, Def2;
then c,a9 // c,x by A19, A21, AFF_1:5;
then LIN c,a9,x by AFF_1:def_1;
then A28: LIN a9,x,c by AFF_1:6;
A29: LIN a9,x,x by AFF_1:7;
assume A30: not a9 in N ; ::_thesis: contradiction
LIN a9,x,b by A25, AFF_1:6;
then x in M by A2, A13, A14, A20, A30, A24, A28, A29, AFF_1:8, AFF_1:25;
hence contradiction by A2, A3, A4, A5, A6, A24, A27, AFF_1:18; ::_thesis: verum
end;
end;
assume A31: AP is satisfying_PAP_1 ; ::_thesis: AP is Pappian
let M be Subset of AP; :: according to AFF_2:def_2 ::_thesis: for N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A32: M is being_line and
A33: N is being_line and
A34: ( M <> N & o in M & o in N ) and
A35: o <> a and
A36: o <> a9 and
A37: o <> b and
A38: o <> b9 and
A39: ( o <> c & o <> c9 ) and
A40: a in M and
A41: b in M and
A42: c in M and
A43: a9 in N and
A44: b9 in N and
A45: c9 in N and
A46: a,b9 // b,a9 and
A47: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9
set A = Line (a,c9);
set P = Line (b,a9);
A48: b <> a9 by A32, A33, A34, A36, A41, A43, AFF_1:18;
then A49: b in Line (b,a9) by AFF_1:24;
assume A50: not a,c9 // c,a9 ; ::_thesis: contradiction
then A51: a <> c9 by AFF_1:3;
then A52: ( a in Line (a,c9) & c9 in Line (a,c9) ) by AFF_1:24;
A53: a9 in Line (b,a9) by A48, AFF_1:24;
Line (a,c9) is being_line by A51, AFF_1:24;
then consider K being Subset of AP such that
A54: c in K and
A55: Line (a,c9) // K by AFF_1:49;
A56: b <> c
proof
assume A57: b = c ; ::_thesis: contradiction
then LIN b,c9,b9 by A47, AFF_1:def_1;
then LIN b9,c9,b by AFF_1:6;
then ( b9 = c9 or b in N ) by A33, A44, A45, AFF_1:25;
hence contradiction by A32, A33, A34, A37, A41, A46, A50, A57, AFF_1:18; ::_thesis: verum
end;
A58: b9 <> c9
proof
assume b9 = c9 ; ::_thesis: contradiction
then b9,b // b9,c by A47, AFF_1:4;
then LIN b9,b,c by AFF_1:def_1;
then LIN b,c,b9 by AFF_1:6;
then b9 in M by A32, A41, A42, A56, AFF_1:25;
hence contradiction by A32, A33, A34, A38, A44, AFF_1:18; ::_thesis: verum
end;
A59: not Line (b,a9) // K
proof
assume Line (b,a9) // K ; ::_thesis: contradiction
then Line (b,a9) // Line (a,c9) by A55, AFF_1:44;
then b,a9 // a,c9 by A52, A49, A53, AFF_1:39;
then a,b9 // a,c9 by A46, A48, AFF_1:5;
then LIN a,b9,c9 by AFF_1:def_1;
then LIN b9,c9,a by AFF_1:6;
then a in N by A33, A44, A45, A58, AFF_1:25;
hence contradiction by A32, A33, A34, A35, A40, AFF_1:18; ::_thesis: verum
end;
A60: Line (b,a9) is being_line by A48, AFF_1:24;
K is being_line by A55, AFF_1:36;
then consider x being Element of AP such that
A61: x in Line (b,a9) and
A62: x in K by A60, A59, AFF_1:58;
A63: a,c9 // c,x by A52, A54, A55, A62, AFF_1:39;
LIN b,x,a9 by A60, A49, A53, A61, AFF_1:21;
then b,x // b,a9 by AFF_1:def_1;
then a,b9 // b,x by A46, A48, AFF_1:5;
then x in N by A31, A32, A33, A34, A35, A37, A38, A39, A40, A41, A42, A44, A45, A47, A56, A63, Def3;
then N = Line (b,a9) by A33, A43, A50, A60, A53, A61, A63, AFF_1:18;
hence contradiction by A32, A33, A34, A37, A41, A49, AFF_1:18; ::_thesis: verum
end;
theorem :: AFF_2:2
for AP being AffinPlane holds
( AP is Desarguesian iff AP is satisfying_DES_1 )
proof
let AP be AffinPlane; ::_thesis: ( AP is Desarguesian iff AP is satisfying_DES_1 )
hereby ::_thesis: ( AP is satisfying_DES_1 implies AP is Desarguesian )
assume A1: AP is Desarguesian ; ::_thesis: AP is satisfying_DES_1
thus AP is satisfying_DES_1 ::_thesis: verum
proof
let A be Subset of AP; :: according to AFF_2:def_5 ::_thesis: for P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
o in C
let P, C be Subset of AP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
o in C
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies o in C )
assume that
A2: o in A and
A3: o in P and
A4: o <> a and
A5: o <> b and
o <> c and
A6: a in A and
A7: a9 in A and
A8: b in P and
A9: b9 in P and
A10: c in C and
A11: c9 in C and
A12: A is being_line and
A13: P is being_line and
A14: C is being_line and
A15: A <> P and
A16: A <> C and
A17: a,b // a9,b9 and
A18: a,c // a9,c9 and
A19: b,c // b9,c9 and
A20: not LIN a,b,c and
A21: c <> c9 ; ::_thesis: o in C
set K = Line (o,c9);
assume A22: not o in C ; ::_thesis: contradiction
then A23: Line (o,c9) is being_line by A11, AFF_1:24;
A24: a9 <> c9
proof
assume A25: a9 = c9 ; ::_thesis: contradiction
then b,c // a9,b9 by A19, AFF_1:4;
then ( a,b // b,c or a9 = b9 ) by A17, AFF_1:5;
then ( b,a // b,c or a9 = b9 ) by AFF_1:4;
then ( LIN b,a,c or a9 = b9 ) by AFF_1:def_1;
hence contradiction by A2, A3, A7, A9, A11, A12, A13, A15, A20, A22, A25, AFF_1:6, AFF_1:18; ::_thesis: verum
end;
A26: A <> Line (o,c9)
proof
assume A = Line (o,c9) ; ::_thesis: contradiction
then A27: c9 in A by A2, AFF_1:24;
a9,c9 // a,c by A18, AFF_1:4;
then c in A by A6, A7, A12, A24, A27, AFF_1:48;
hence contradiction by A10, A11, A12, A14, A16, A21, A27, AFF_1:18; ::_thesis: verum
end;
A28: a <> c by A20, AFF_1:7;
A29: o in Line (o,c9) by A11, A22, AFF_1:24;
A30: c9 in Line (o,c9) by A11, A22, AFF_1:24;
not a,c // Line (o,c9)
proof
assume a,c // Line (o,c9) ; ::_thesis: contradiction
then a9,c9 // Line (o,c9) by A18, A28, AFF_1:32;
then c9,a9 // Line (o,c9) by AFF_1:34;
then a9 in Line (o,c9) by A23, A30, AFF_1:23;
then A31: a9 in P by A2, A3, A7, A12, A23, A29, A26, AFF_1:18;
a9,b9 // b,a by A17, AFF_1:4;
then ( a9 = b9 or a in P ) by A8, A9, A13, A31, AFF_1:48;
then a,c // b,c by A2, A3, A4, A6, A12, A13, A15, A18, A19, A24, AFF_1:5, AFF_1:18;
then c,a // c,b by AFF_1:4;
then LIN c,a,b by AFF_1:def_1;
hence contradiction by A20, AFF_1:6; ::_thesis: verum
end;
then consider x being Element of AP such that
A32: x in Line (o,c9) and
A33: LIN a,c,x by A23, AFF_1:59;
A34: o <> x
proof
assume o = x ; ::_thesis: contradiction
then LIN a,o,c by A33, AFF_1:6;
then A35: c in A by A2, A4, A6, A12, AFF_1:25;
then c9 in A by A6, A7, A12, A18, A28, AFF_1:48;
hence contradiction by A10, A11, A12, A14, A16, A21, A35, AFF_1:18; ::_thesis: verum
end;
A36: b9 <> c9
proof
assume b9 = c9 ; ::_thesis: contradiction
then ( a9 = b9 or a,c // a,b ) by A17, A18, AFF_1:5;
then ( a9 = b9 or LIN a,c,b ) by AFF_1:def_1;
then b,c // a,c by A18, A19, A20, A24, AFF_1:5, AFF_1:6;
then c,b // c,a by AFF_1:4;
then LIN c,b,a by AFF_1:def_1;
hence contradiction by A20, AFF_1:6; ::_thesis: verum
end;
A37: a,c // a,x by A33, AFF_1:def_1;
then a,x // a9,c9 by A18, A28, AFF_1:5;
then b,x // b9,c9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A15, A17, A23, A29, A30, A26, A32, A34, Def4;
then A38: b,x // b,c by A19, A36, AFF_1:5;
A39: not LIN a,b,x
proof
assume LIN a,b,x ; ::_thesis: contradiction
then a,b // a,x by AFF_1:def_1;
then ( a,b // a,c or a = x ) by A37, AFF_1:5;
hence contradiction by A2, A4, A6, A12, A20, A23, A29, A26, A32, AFF_1:18, AFF_1:def_1; ::_thesis: verum
end;
LIN a,x,c by A33, AFF_1:6;
then c in Line (o,c9) by A32, A39, A38, AFF_1:14;
hence contradiction by A10, A11, A14, A21, A22, A23, A29, A30, AFF_1:18; ::_thesis: verum
end;
end;
assume A40: AP is satisfying_DES_1 ; ::_thesis: AP is Desarguesian
let A be Subset of AP; :: according to AFF_2:def_4 ::_thesis: for P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let P, C be Subset of AP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A41: o in A and
A42: o in P and
A43: o in C and
A44: o <> a and
A45: o <> b and
A46: o <> c and
A47: a in A and
A48: a9 in A and
A49: b in P and
A50: b9 in P and
A51: c in C and
A52: c9 in C and
A53: A is being_line and
A54: P is being_line and
A55: C is being_line and
A56: A <> P and
A57: A <> C and
A58: a,b // a9,b9 and
A59: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
assume A60: not b,c // b9,c9 ; ::_thesis: contradiction
A61: a9 <> b9
proof
A62: a9,c9 // c,a by A59, AFF_1:4;
assume A63: a9 = b9 ; ::_thesis: contradiction
then a9 in C by A41, A42, A43, A48, A50, A53, A54, A56, AFF_1:18;
then ( a in C or a9 = c9 ) by A51, A52, A55, A62, AFF_1:48;
hence contradiction by A41, A43, A44, A47, A53, A55, A57, A60, A63, AFF_1:3, AFF_1:18; ::_thesis: verum
end;
A64: a9 <> c9
proof
assume a9 = c9 ; ::_thesis: contradiction
then A65: a9 in P by A41, A42, A43, A48, A52, A53, A55, A57, AFF_1:18;
a9,b9 // b,a by A58, AFF_1:4;
then a in P by A49, A50, A54, A61, A65, AFF_1:48;
hence contradiction by A41, A42, A44, A47, A53, A54, A56, AFF_1:18; ::_thesis: verum
end;
A66: o <> c9
proof
assume A67: o = c9 ; ::_thesis: contradiction
a9,c9 // a,c by A59, AFF_1:4;
then c in A by A41, A47, A48, A53, A64, A67, AFF_1:48;
hence contradiction by A41, A43, A46, A51, A53, A55, A57, AFF_1:18; ::_thesis: verum
end;
set M = Line (a,c);
set N = Line (b9,c9);
A68: a <> c by A41, A43, A44, A47, A51, A53, A55, A57, AFF_1:18;
then A69: c in Line (a,c) by AFF_1:24;
A70: a <> b by A41, A42, A44, A47, A49, A53, A54, A56, AFF_1:18;
A71: not LIN a9,b9,c9
proof
assume A72: LIN a9,b9,c9 ; ::_thesis: contradiction
then a9,b9 // a9,c9 by AFF_1:def_1;
then a9,b9 // a,c by A59, A64, AFF_1:5;
then a,b // a,c by A58, A61, AFF_1:5;
then LIN a,b,c by AFF_1:def_1;
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def_1;
then b,c // a,b by AFF_1:4;
then A73: b,c // a9,b9 by A58, A70, AFF_1:5;
LIN b9,c9,a9 by A72, AFF_1:6;
then b9,c9 // b9,a9 by AFF_1:def_1;
then b9,c9 // a9,b9 by AFF_1:4;
hence contradiction by A60, A61, A73, AFF_1:5; ::_thesis: verum
end;
A74: b9 <> c9 by A60, AFF_1:3;
then A75: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:24;
Line (b9,c9) is being_line by A74, AFF_1:24;
then consider D being Subset of AP such that
A76: b in D and
A77: Line (b9,c9) // D by AFF_1:49;
A78: a in Line (a,c) by A68, AFF_1:24;
A79: not Line (a,c) // D
proof
assume Line (a,c) // D ; ::_thesis: contradiction
then Line (a,c) // Line (b9,c9) by A77, AFF_1:44;
then a,c // b9,c9 by A78, A69, A75, AFF_1:39;
then a9,c9 // b9,c9 by A59, A68, AFF_1:5;
then c9,a9 // c9,b9 by AFF_1:4;
then LIN c9,a9,b9 by AFF_1:def_1;
hence contradiction by A71, AFF_1:6; ::_thesis: verum
end;
A80: Line (a,c) is being_line by A68, AFF_1:24;
D is being_line by A77, AFF_1:36;
then consider x being Element of AP such that
A81: x in Line (a,c) and
A82: x in D by A80, A79, AFF_1:58;
LIN a,c,x by A80, A78, A69, A81, AFF_1:21;
then a,c // a,x by AFF_1:def_1;
then A83: a,x // a9,c9 by A59, A68, AFF_1:5;
set T = Line (c9,x);
A84: a <> a9
proof
assume A85: a = a9 ; ::_thesis: contradiction
then LIN a,c,c9 by A59, AFF_1:def_1;
then LIN c,c9,a by AFF_1:6;
then A86: ( c = c9 or a in C ) by A51, A52, A55, AFF_1:25;
LIN a,b,b9 by A58, A85, AFF_1:def_1;
then LIN b,b9,a by AFF_1:6;
then ( b = b9 or a in P ) by A49, A50, A54, AFF_1:25;
hence contradiction by A41, A42, A43, A44, A47, A53, A54, A55, A56, A57, A60, A86, AFF_1:2, AFF_1:18; ::_thesis: verum
end;
A87: x <> c9
proof
assume x = c9 ; ::_thesis: contradiction
then c9,a // c9,a9 by A83, AFF_1:4;
then LIN c9,a,a9 by AFF_1:def_1;
then LIN a,a9,c9 by AFF_1:6;
then c9 in A by A47, A48, A53, A84, AFF_1:25;
hence contradiction by A41, A43, A52, A53, A55, A57, A66, AFF_1:18; ::_thesis: verum
end;
then A88: ( Line (c9,x) is being_line & c9 in Line (c9,x) ) by AFF_1:24;
A89: b,x // b9,c9 by A75, A76, A77, A82, AFF_1:39;
A90: x in Line (c9,x) by A87, AFF_1:24;
A91: a <> x
proof
assume a = x ; ::_thesis: contradiction
then a,b // b9,c9 by A75, A76, A77, A82, AFF_1:39;
then a9,b9 // b9,c9 by A58, A70, AFF_1:5;
then b9,a9 // b9,c9 by AFF_1:4;
then LIN b9,a9,c9 by AFF_1:def_1;
hence contradiction by A71, AFF_1:6; ::_thesis: verum
end;
not LIN a,b,x
proof
assume LIN a,b,x ; ::_thesis: contradiction
then a,b // a,x by AFF_1:def_1;
then a,b // a9,c9 by A83, A91, AFF_1:5;
then a9,b9 // a9,c9 by A58, A70, AFF_1:5;
hence contradiction by A71, AFF_1:def_1; ::_thesis: verum
end;
then o in Line (c9,x) by A40, A41, A42, A44, A45, A47, A48, A49, A50, A53, A54, A56, A58, A83, A89, A87, A88, A90, Def5;
then x in C by A43, A52, A55, A66, A88, A90, AFF_1:18;
then C = Line (a,c) by A51, A55, A60, A80, A69, A81, A89, AFF_1:18;
hence contradiction by A41, A43, A44, A47, A53, A55, A57, A78, AFF_1:18; ::_thesis: verum
end;
theorem Th3: :: AFF_2:3
for AP being AffinPlane st AP is Moufangian holds
AP is satisfying_TDES_1
proof
let AP be AffinPlane; ::_thesis: ( AP is Moufangian implies AP is satisfying_TDES_1 )
assume A1: AP is Moufangian ; ::_thesis: AP is satisfying_TDES_1
let K be Subset of AP; :: according to AFF_2:def_8 ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
LIN o,b,b9
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K implies LIN o,b,b9 )
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: o <> c and
A8: a <> b and
A9: LIN o,a,a9 and
A10: a,b // a9,b9 and
A11: b,c // b9,c9 and
A12: a,c // a9,c9 and
A13: a,b // K ; ::_thesis: LIN o,b,b9
consider P being Subset of AP such that
A14: a9 in P and
A15: K // P by A2, AFF_1:49;
A16: P is being_line by A15, AFF_1:36;
set A = Line (o,b);
set C = Line (o,a);
A17: ( o in Line (o,b) & b in Line (o,b) ) by AFF_1:15;
assume A18: not LIN o,b,b9 ; ::_thesis: contradiction
then o <> b by AFF_1:7;
then A19: Line (o,b) is being_line by AFF_1:def_3;
A20: not b in K by A6, A13, AFF_1:35;
not Line (o,b) // P
proof
assume Line (o,b) // P ; ::_thesis: contradiction
then Line (o,b) // K by A15, AFF_1:44;
hence contradiction by A3, A20, A17, AFF_1:45; ::_thesis: verum
end;
then consider x being Element of AP such that
A21: x in Line (o,b) and
A22: x in P by A19, A16, AFF_1:58;
A23: ( o in Line (o,a) & a in Line (o,a) ) by AFF_1:15;
A24: LIN o,b,x by A19, A17, A21, AFF_1:21;
a,b // P by A13, A15, AFF_1:43;
then a9,b9 // P by A8, A10, AFF_1:32;
then A25: b9 in P by A14, A16, AFF_1:23;
then A26: LIN b9,x,b9 by A16, A22, AFF_1:21;
A27: Line (o,a) is being_line by A3, A6, AFF_1:def_3;
then A28: a9 in Line (o,a) by A3, A6, A9, A23, AFF_1:25;
A29: b9 <> c9
proof
A30: a9,c9 // c,a by A12, AFF_1:4;
assume A31: b9 = c9 ; ::_thesis: contradiction
then P = K by A5, A15, A25, AFF_1:45;
then a9 = o by A2, A3, A6, A27, A23, A28, A14, AFF_1:18;
then b9 = o by A2, A3, A4, A5, A6, A31, A30, AFF_1:48;
hence contradiction by A18, AFF_1:7; ::_thesis: verum
end;
A32: b <> c by A4, A6, A13, AFF_1:35;
a9,x // K by A14, A15, A22, AFF_1:40;
then a,b // a9,x by A2, A13, AFF_1:31;
then b,c // x,c9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A24, Def7;
then b9,c9 // x,c9 by A11, A32, AFF_1:5;
then c9,b9 // c9,x by AFF_1:4;
then LIN c9,b9,x by AFF_1:def_1;
then A33: LIN b9,x,c9 by AFF_1:6;
A34: a9 <> b9
proof
assume A35: a9 = b9 ; ::_thesis: contradiction
A36: now__::_thesis:_not_a9_=_c9
assume a9 = c9 ; ::_thesis: contradiction
then b9 = o by A2, A3, A5, A6, A27, A23, A28, A35, AFF_1:18;
hence contradiction by A18, AFF_1:7; ::_thesis: verum
end;
( a,c // b,c or a9 = c9 ) by A11, A12, A35, AFF_1:5;
then c,a // c,b by A36, AFF_1:4;
then LIN c,a,b by AFF_1:def_1;
then LIN a,c,b by AFF_1:6;
then a,c // a,b by AFF_1:def_1;
then a,b // a,c by AFF_1:4;
then a,c // K by A8, A13, AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2, A4, A6, AFF_1:23; ::_thesis: verum
end;
LIN b9,x,a9 by A14, A16, A22, A25, AFF_1:21;
then LIN b9,c9,a9 by A18, A24, A33, A26, AFF_1:8;
then b9,c9 // b9,a9 by AFF_1:def_1;
then b9,c9 // a9,b9 by AFF_1:4;
then b,c // a9,b9 by A11, A29, AFF_1:5;
then a,b // b,c by A10, A34, AFF_1:5;
then b,c // K by A8, A13, AFF_1:32;
then c,b // K by AFF_1:34;
hence contradiction by A2, A4, A20, AFF_1:23; ::_thesis: verum
end;
theorem :: AFF_2:4
for AP being AffinPlane st AP is satisfying_TDES_1 holds
AP is satisfying_TDES_2
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_TDES_1 implies AP is satisfying_TDES_2 )
assume A1: AP is satisfying_TDES_1 ; ::_thesis: AP is satisfying_TDES_2
let K be Subset of AP; :: according to AFF_2:def_9 ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds
a,b // a9,b9
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K implies a,b // a9,b9 )
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: o <> c and
A8: a <> b and
A9: LIN o,a,a9 and
A10: LIN o,b,b9 and
A11: b,c // b9,c9 and
A12: a,c // a9,c9 and
A13: a,b // K ; ::_thesis: a,b // a9,b9
set A = Line (o,a);
set P = Line (o,b);
A14: ( Line (o,a) is being_line & a in Line (o,a) ) by A3, A6, AFF_1:24;
A15: o in Line (o,a) by A3, A6, AFF_1:24;
then A16: a9 in Line (o,a) by A3, A6, A9, A14, AFF_1:25;
A17: o <> b by A3, A6, A13, AFF_1:35;
then A18: Line (o,b) is being_line by AFF_1:24;
consider N being Subset of AP such that
A19: a9 in N and
A20: K // N by A2, AFF_1:49;
A21: N is being_line by A20, AFF_1:36;
set T = Line (b9,c9);
A22: not b in K by A6, A13, AFF_1:35;
A23: b in Line (o,b) by A17, AFF_1:24;
A24: o in Line (o,b) by A17, AFF_1:24;
then A25: b9 in Line (o,b) by A10, A17, A18, A23, AFF_1:25;
assume A26: not a,b // a9,b9 ; ::_thesis: contradiction
then A27: a9 <> b9 by AFF_1:3;
A28: not b9 in K
proof
A29: a9,c9 // a,c by A12, AFF_1:4;
A30: b9,c9 // c,b by A11, AFF_1:4;
assume A31: b9 in K ; ::_thesis: contradiction
then b9 = o by A2, A3, A22, A18, A24, A23, A25, AFF_1:18;
then c9 in Line (o,a) by A2, A3, A4, A5, A22, A15, A30, AFF_1:48;
then ( a9 = c9 or c in Line (o,a) ) by A14, A16, A29, AFF_1:48;
hence contradiction by A2, A3, A4, A5, A6, A7, A27, A22, A15, A14, A31, A30, AFF_1:18, AFF_1:48; ::_thesis: verum
end;
then A32: Line (b9,c9) is being_line by A5, AFF_1:24;
A33: b9 in Line (b9,c9) by A5, A28, AFF_1:24;
A34: c9 in Line (b9,c9) by A5, A28, AFF_1:24;
not N // Line (b9,c9)
proof
assume N // Line (b9,c9) ; ::_thesis: contradiction
then K // Line (b9,c9) by A20, AFF_1:44;
hence contradiction by A5, A28, A33, A34, AFF_1:45; ::_thesis: verum
end;
then consider x being Element of AP such that
A35: x in N and
A36: x in Line (b9,c9) by A32, A21, AFF_1:58;
a9,x // K by A19, A20, A35, AFF_1:40;
then A37: a,b // a9,x by A2, A13, AFF_1:31;
LIN c9,b9,x by A32, A33, A34, A36, AFF_1:21;
then c9,b9 // c9,x by AFF_1:def_1;
then b9,c9 // x,c9 by AFF_1:4;
then b,c // x,c9 by A5, A11, A28, AFF_1:5;
then LIN o,b,x by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A37, Def8;
then x in Line (o,b) by A17, A18, A24, A23, AFF_1:25;
then Line (o,b) = Line (b9,c9) by A26, A18, A25, A32, A33, A36, A37, AFF_1:18;
then LIN c9,b9,b by A18, A23, A33, A34, AFF_1:21;
then c9,b9 // c9,b by AFF_1:def_1;
then b9,c9 // b,c9 by AFF_1:4;
then b,c // b,c9 by A5, A11, A28, AFF_1:5;
then LIN b,c,c9 by AFF_1:def_1;
then A38: LIN c,c9,b by AFF_1:6;
then a,c // a9,c by A2, A4, A5, A12, A22, AFF_1:25;
then c,a // c,a9 by AFF_1:4;
then LIN c,a,a9 by AFF_1:def_1;
then LIN a,a9,c by AFF_1:6;
then A39: ( a = a9 or c in Line (o,a) ) by A14, A16, AFF_1:25;
b,c // b9,c by A2, A4, A5, A11, A22, A38, AFF_1:25;
then c,b // c,b9 by AFF_1:4;
then LIN c,b,b9 by AFF_1:def_1;
then LIN b,b9,c by AFF_1:6;
then ( b = b9 or c in Line (o,b) ) by A18, A23, A25, AFF_1:25;
hence contradiction by A2, A3, A4, A6, A7, A26, A22, A18, A15, A14, A24, A23, A39, AFF_1:2, AFF_1:18; ::_thesis: verum
end;
theorem :: AFF_2:5
for AP being AffinPlane st AP is satisfying_TDES_2 holds
AP is satisfying_TDES_3
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_TDES_2 implies AP is satisfying_TDES_3 )
assume A1: AP is satisfying_TDES_2 ; ::_thesis: AP is satisfying_TDES_3
let K be Subset of AP; :: according to AFF_2:def_10 ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & a,b // K holds
c9 in K
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & a,b // K implies c9 in K )
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: not a in K and
A6: o <> c and
A7: a <> b and
A8: LIN o,a,a9 and
A9: LIN o,b,b9 and
A10: a,b // a9,b9 and
A11: a,c // a9,c9 and
A12: b,c // b9,c9 and
A13: a,b // K ; ::_thesis: c9 in K
set A = Line (o,a);
set P = Line (o,b);
set N = Line (b,c);
A14: o in Line (o,a) by A3, A5, AFF_1:24;
A15: not LIN a,b,c
proof
assume LIN a,b,c ; ::_thesis: contradiction
then a,b // a,c by AFF_1:def_1;
then a,c // K by A7, A13, AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2, A4, A5, AFF_1:23; ::_thesis: verum
end;
A16: o <> b by A3, A5, A13, AFF_1:35;
then A17: b in Line (o,b) by AFF_1:24;
A18: a9,b9 // b,a by A10, AFF_1:4;
A19: b <> c by A4, A5, A13, AFF_1:35;
then A20: ( b in Line (b,c) & c in Line (b,c) ) by AFF_1:24;
A21: a in Line (o,a) by A3, A5, AFF_1:24;
A22: Line (o,a) is being_line by A3, A5, AFF_1:24;
A23: Line (o,a) <> Line (o,b)
proof
assume Line (o,a) = Line (o,b) ; ::_thesis: contradiction
then a,b // Line (o,a) by A22, A21, A17, AFF_1:40, AFF_1:41;
hence contradiction by A3, A5, A7, A13, A14, A21, AFF_1:45, AFF_1:53; ::_thesis: verum
end;
assume A24: not c9 in K ; ::_thesis: contradiction
A25: Line (o,b) is being_line by A16, AFF_1:24;
A26: o in Line (o,b) by A16, AFF_1:24;
then A27: b9 in Line (o,b) by A9, A16, A25, A17, AFF_1:25;
A28: a9 in Line (o,a) by A3, A5, A8, A22, A14, A21, AFF_1:25;
A29: a9 <> b9
proof
assume A30: a9 = b9 ; ::_thesis: contradiction
then ( a,c // b,c or a9 = c9 ) by A11, A12, AFF_1:5;
then ( c,a // c,b or a9 = c9 ) by AFF_1:4;
then ( LIN c,a,b or a9 = c9 ) by AFF_1:def_1;
hence contradiction by A3, A24, A15, A22, A25, A14, A26, A28, A27, A23, A30, AFF_1:6, AFF_1:18; ::_thesis: verum
end;
A31: a9 <> c9
proof
assume a9 = c9 ; ::_thesis: contradiction
then b,c // a9,b9 by A12, AFF_1:4;
then a,b // b,c by A10, A29, AFF_1:5;
then b,a // b,c by AFF_1:4;
then LIN b,a,c by AFF_1:def_1;
hence contradiction by A15, AFF_1:6; ::_thesis: verum
end;
not a9,c9 // K
proof
assume A32: a9,c9 // K ; ::_thesis: contradiction
a9,c9 // a,c by A11, AFF_1:4;
then a,c // K by A31, A32, AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2, A4, A5, AFF_1:23; ::_thesis: verum
end;
then consider x being Element of AP such that
A33: x in K and
A34: LIN a9,c9,x by A2, AFF_1:59;
a9,c9 // a9,x by A34, AFF_1:def_1;
then A35: a,c // a9,x by A11, A31, AFF_1:5;
Line (b,c) is being_line by A19, AFF_1:24;
then consider T being Subset of AP such that
A36: x in T and
A37: Line (b,c) // T by AFF_1:49;
A38: not b in K by A5, A13, AFF_1:35;
A39: not T // Line (o,b)
proof
assume T // Line (o,b) ; ::_thesis: contradiction
then Line (b,c) // Line (o,b) by A37, AFF_1:44;
then c in Line (o,b) by A17, A20, AFF_1:45;
hence contradiction by A2, A3, A4, A6, A38, A25, A26, A17, AFF_1:18; ::_thesis: verum
end;
T is being_line by A37, AFF_1:36;
then consider y being Element of AP such that
A40: y in T and
A41: y in Line (o,b) by A25, A39, AFF_1:58;
A42: b,c // y,x by A20, A36, A37, A40, AFF_1:39;
A43: now__::_thesis:_not_y_=_b9
assume y = b9 ; ::_thesis: contradiction
then b9,c9 // b9,x by A12, A19, A42, AFF_1:5;
then LIN b9,c9,x by AFF_1:def_1;
then A44: LIN c9,x,b9 by AFF_1:6;
( LIN c9,x,a9 & LIN c9,x,c9 ) by A34, AFF_1:6, AFF_1:7;
then LIN a9,b9,c9 by A24, A33, A44, AFF_1:8;
then a9,b9 // a9,c9 by AFF_1:def_1;
then a9,b9 // a,c by A11, A31, AFF_1:5;
then a,b // a,c by A10, A29, AFF_1:5;
hence contradiction by A15, AFF_1:def_1; ::_thesis: verum
end;
LIN o,b,y by A25, A26, A17, A41, AFF_1:21;
then a,b // a9,y by A1, A2, A3, A4, A5, A6, A7, A8, A13, A33, A42, A35, Def9;
then a9,b9 // a9,y by A7, A10, AFF_1:5;
then LIN a9,b9,y by AFF_1:def_1;
then LIN b9,y,a9 by AFF_1:6;
then a9 in Line (o,b) by A25, A27, A41, A43, AFF_1:25;
then a in Line (o,b) by A25, A17, A27, A29, A18, AFF_1:48;
hence contradiction by A3, A5, A25, A26, A23, AFF_1:24; ::_thesis: verum
end;
theorem :: AFF_2:6
for AP being AffinPlane st AP is satisfying_TDES_3 holds
AP is Moufangian
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_TDES_3 implies AP is Moufangian )
assume A1: AP is satisfying_TDES_3 ; ::_thesis: AP is Moufangian
let K be Subset of AP; :: according to AFF_2:def_7 ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )
assume that
A2: K is being_line and
A3: o in K and
A4: c in K and
A5: c9 in K and
A6: not a in K and
A7: o <> c and
A8: a <> b and
A9: LIN o,a,a9 and
A10: LIN o,b,b9 and
A11: a,b // a9,b9 and
A12: a,c // a9,c9 and
A13: a,b // K ; ::_thesis: b,c // b9,c9
set A = Line (o,a);
set P = Line (o,b);
set M = Line (b,c);
set T = Line (a9,c9);
A14: o in Line (o,a) by A3, A6, AFF_1:24;
assume A15: not b,c // b9,c9 ; ::_thesis: contradiction
then A16: b <> c by AFF_1:3;
then A17: b in Line (b,c) by AFF_1:24;
A18: a9,b9 // b,a by A11, AFF_1:4;
A19: c in Line (b,c) by A16, AFF_1:24;
A20: a in Line (o,a) by A3, A6, AFF_1:24;
A21: Line (o,a) is being_line by A3, A6, AFF_1:24;
then A22: a9 in Line (o,a) by A3, A6, A9, A14, A20, AFF_1:25;
A23: o <> b by A3, A6, A13, AFF_1:35;
then A24: Line (o,b) is being_line by AFF_1:24;
A25: b in Line (o,b) by A23, AFF_1:24;
A26: Line (o,a) <> Line (o,b)
proof
assume Line (o,a) = Line (o,b) ; ::_thesis: contradiction
then a,b // Line (o,a) by A21, A20, A25, AFF_1:40, AFF_1:41;
hence contradiction by A3, A6, A8, A13, A14, A20, AFF_1:45, AFF_1:53; ::_thesis: verum
end;
A27: o in Line (o,b) by A23, AFF_1:24;
then A28: b9 in Line (o,b) by A10, A23, A24, A25, AFF_1:25;
A29: a9 <> b9
proof
A30: a9,c9 // c,a by A12, AFF_1:4;
assume A31: a9 = b9 ; ::_thesis: contradiction
then a9 in K by A3, A21, A24, A14, A27, A22, A28, A26, AFF_1:18;
then a9 = c9 by A2, A4, A5, A6, A30, AFF_1:48;
hence contradiction by A15, A31, AFF_1:3; ::_thesis: verum
end;
A32: a9 <> c9
proof
assume a9 = c9 ; ::_thesis: contradiction
then A33: a9 in Line (o,b) by A2, A3, A5, A6, A21, A14, A20, A27, A22, AFF_1:18;
a9,b9 // b,a by A11, AFF_1:4;
then a in Line (o,b) by A24, A25, A28, A29, A33, AFF_1:48;
hence contradiction by A3, A6, A24, A27, A26, AFF_1:24; ::_thesis: verum
end;
then A34: ( Line (a9,c9) is being_line & c9 in Line (a9,c9) ) by AFF_1:24;
A35: Line (b,c) is being_line by A16, AFF_1:24;
then consider N being Subset of AP such that
A36: b9 in N and
A37: Line (b,c) // N by AFF_1:49;
A38: N is being_line by A37, AFF_1:36;
A39: not LIN a,b,c
proof
assume LIN a,b,c ; ::_thesis: contradiction
then a,b // a,c by AFF_1:def_1;
then a,c // K by A8, A13, AFF_1:32;
then c,a // K by AFF_1:34;
hence contradiction by A2, A4, A6, AFF_1:23; ::_thesis: verum
end;
not a9,c9 // N
proof
assume A40: a9,c9 // N ; ::_thesis: contradiction
a9,c9 // a,c by A12, AFF_1:4;
then a,c // N by A32, A40, AFF_1:32;
then a,c // Line (b,c) by A37, AFF_1:43;
then c,a // Line (b,c) by AFF_1:34;
then a in Line (b,c) by A35, A19, AFF_1:23;
hence contradiction by A39, A35, A17, A19, AFF_1:21; ::_thesis: verum
end;
then consider x being Element of AP such that
A41: x in N and
A42: LIN a9,c9,x by A38, AFF_1:59;
A43: b,c // b9,x by A17, A19, A36, A37, A41, AFF_1:39;
a9,c9 // a9,x by A42, AFF_1:def_1;
then a,c // a9,x by A12, A32, AFF_1:5;
then A44: x in K by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A13, A43, Def10;
A45: a9 in Line (a9,c9) by A32, AFF_1:24;
then x in Line (a9,c9) by A32, A34, A42, AFF_1:25;
then K = Line (a9,c9) by A2, A5, A15, A34, A43, A44, AFF_1:18;
then a9 in Line (o,b) by A2, A3, A6, A21, A14, A20, A27, A22, A45, AFF_1:18;
then a in Line (o,b) by A24, A25, A28, A29, A18, AFF_1:48;
hence contradiction by A3, A6, A24, A27, A26, AFF_1:24; ::_thesis: verum
end;
theorem Th7: :: AFF_2:7
for AP being AffinPlane holds
( AP is translational iff AP is satisfying_des_1 )
proof
let AP be AffinPlane; ::_thesis: ( AP is translational iff AP is satisfying_des_1 )
hereby ::_thesis: ( AP is satisfying_des_1 implies AP is translational )
assume A1: AP is translational ; ::_thesis: AP is satisfying_des_1
thus AP is satisfying_des_1 ::_thesis: verum
proof
let A be Subset of AP; :: according to AFF_2:def_12 ::_thesis: for P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let P, C be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies A // C )
assume that
A2: A // P and
A3: a in A and
A4: a9 in A and
A5: b in P and
A6: b9 in P and
A7: ( c in C & c9 in C ) and
A8: A is being_line and
A9: P is being_line and
A10: C is being_line and
A11: A <> P and
A12: A <> C and
A13: a,b // a9,b9 and
A14: a,c // a9,c9 and
A15: b,c // b9,c9 and
A16: not LIN a,b,c and
A17: c <> c9 ; ::_thesis: A // C
assume A18: not A // C ; ::_thesis: contradiction
consider K being Subset of AP such that
A19: c9 in K and
A20: A // K by A8, AFF_1:49;
A21: a <> c by A16, AFF_1:7;
A22: not a,c // K
proof
assume a,c // K ; ::_thesis: contradiction
then a,c // A by A20, AFF_1:43;
then A23: c in A by A3, A8, AFF_1:23;
a9,c9 // a,c by A14, AFF_1:4;
then a9,c9 // A by A3, A8, A21, A23, AFF_1:27;
then c9 in A by A4, A8, AFF_1:23;
hence contradiction by A7, A8, A10, A12, A17, A23, AFF_1:18; ::_thesis: verum
end;
A24: A <> K
proof
assume A25: A = K ; ::_thesis: contradiction
a9,c9 // a,c by A14, AFF_1:4;
then a9 = c9 by A4, A19, A20, A22, A25, AFF_1:32, AFF_1:40;
then a9,b9 // b,c by A15, AFF_1:4;
then ( a9 = b9 or a,b // b,c ) by A13, AFF_1:5;
then ( b9 in A or b,a // b,c ) by A4, AFF_1:4;
then LIN b,a,c by A2, A6, A11, AFF_1:45, AFF_1:def_1;
hence contradiction by A16, AFF_1:6; ::_thesis: verum
end;
A26: now__::_thesis:_not_b9_=_c9
assume b9 = c9 ; ::_thesis: contradiction
then ( a,b // a,c or a9 = b9 ) by A13, A14, AFF_1:5;
hence contradiction by A2, A4, A6, A11, A16, AFF_1:45, AFF_1:def_1; ::_thesis: verum
end;
A27: K is being_line by A20, AFF_1:36;
then consider x being Element of AP such that
A28: x in K and
A29: LIN a,c,x by A22, AFF_1:59;
a,c // a,x by A29, AFF_1:def_1;
then a,x // a9,c9 by A14, A21, AFF_1:5;
then b,x // b9,c9 by A1, A2, A3, A4, A5, A6, A8, A9, A11, A13, A19, A20, A27, A28, A24, Def11;
then ( b,x // b,c or b9 = c9 ) by A15, AFF_1:5;
then LIN b,x,c by A26, AFF_1:def_1;
then A30: LIN x,c,b by AFF_1:6;
A31: LIN x,c,c by AFF_1:7;
LIN x,c,a by A29, AFF_1:6;
then c in K by A16, A28, A30, A31, AFF_1:8;
hence contradiction by A7, A10, A17, A18, A19, A20, A27, AFF_1:18; ::_thesis: verum
end;
end;
assume A32: AP is satisfying_des_1 ; ::_thesis: AP is translational
let A be Subset of AP; :: according to AFF_2:def_11 ::_thesis: for P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let P, C be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A33: A // P and
A34: A // C and
A35: a in A and
A36: a9 in A and
A37: b in P and
A38: b9 in P and
A39: c in C and
A40: c9 in C and
A41: A is being_line and
A42: P is being_line and
A43: C is being_line and
A44: A <> P and
A45: A <> C and
A46: a,b // a9,b9 and
A47: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
A48: a <> b by A33, A35, A37, A44, AFF_1:45;
A49: a9 <> b9 by A33, A36, A38, A44, AFF_1:45;
set K = Line (a,c);
set N = Line (b9,c9);
A50: a <> c by A34, A35, A39, A45, AFF_1:45;
then A51: a in Line (a,c) by AFF_1:24;
assume A52: not b,c // b9,c9 ; ::_thesis: contradiction
then A53: b9 <> c9 by AFF_1:3;
then A54: b9 in Line (b9,c9) by AFF_1:24;
A55: b <> c by A52, AFF_1:3;
A56: not LIN a,b,c
proof
assume A57: LIN a,b,c ; ::_thesis: contradiction
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def_1;
then b,c // a,b by AFF_1:4;
then A58: b,c // a9,b9 by A46, A48, AFF_1:5;
LIN c,b,a by A57, AFF_1:6;
then c,b // c,a by AFF_1:def_1;
then b,c // a,c by AFF_1:4;
then b,c // a9,c9 by A47, A50, AFF_1:5;
then a9,c9 // a9,b9 by A55, A58, AFF_1:5;
then LIN a9,c9,b9 by AFF_1:def_1;
then LIN b9,c9,a9 by AFF_1:6;
then b9,c9 // b9,a9 by AFF_1:def_1;
then b9,c9 // a9,b9 by AFF_1:4;
hence contradiction by A52, A49, A58, AFF_1:5; ::_thesis: verum
end;
A59: c in Line (a,c) by A50, AFF_1:24;
A60: Line (b9,c9) is being_line by A53, AFF_1:24;
then consider M being Subset of AP such that
A61: b in M and
A62: Line (b9,c9) // M by AFF_1:49;
A63: c9 in Line (b9,c9) by A53, AFF_1:24;
A64: a9 <> c9 by A34, A36, A40, A45, AFF_1:45;
A65: not LIN a9,b9,c9
proof
assume LIN a9,b9,c9 ; ::_thesis: contradiction
then a9,b9 // a9,c9 by AFF_1:def_1;
then a,b // a9,c9 by A46, A49, AFF_1:5;
then a,b // a,c by A47, A64, AFF_1:5;
hence contradiction by A56, AFF_1:def_1; ::_thesis: verum
end;
A66: not Line (a,c) // M
proof
assume Line (a,c) // M ; ::_thesis: contradiction
then Line (a,c) // Line (b9,c9) by A62, AFF_1:44;
then a,c // b9,c9 by A51, A59, A54, A63, AFF_1:39;
then a9,c9 // b9,c9 by A47, A50, AFF_1:5;
then c9,a9 // c9,b9 by AFF_1:4;
then LIN c9,a9,b9 by AFF_1:def_1;
hence contradiction by A65, AFF_1:6; ::_thesis: verum
end;
A67: Line (a,c) is being_line by A50, AFF_1:24;
A68: M is being_line by A62, AFF_1:36;
then consider x being Element of AP such that
A69: x in Line (a,c) and
A70: x in M by A67, A66, AFF_1:58;
A71: b,x // b9,c9 by A54, A63, A61, A62, A70, AFF_1:39;
set D = Line (x,c9);
A72: A <> Line (x,c9)
proof
assume A = Line (x,c9) ; ::_thesis: contradiction
then c9 in A by AFF_1:15;
hence contradiction by A34, A40, A45, AFF_1:45; ::_thesis: verum
end;
A73: x in Line (x,c9) by AFF_1:15;
LIN a,c,x by A67, A51, A59, A69, AFF_1:21;
then a,c // a,x by AFF_1:def_1;
then A74: a,x // a9,c9 by A47, A50, AFF_1:5;
A75: c9 in Line (x,c9) by AFF_1:15;
A76: not LIN a,b,x
proof
A77: a <> x
proof
assume a = x ; ::_thesis: contradiction
then a,b // b9,c9 by A54, A63, A61, A62, A70, AFF_1:39;
then a9,b9 // b9,c9 by A46, A48, AFF_1:5;
then b9,a9 // b9,c9 by AFF_1:4;
then LIN b9,a9,c9 by AFF_1:def_1;
hence contradiction by A65, AFF_1:6; ::_thesis: verum
end;
assume LIN a,b,x ; ::_thesis: contradiction
then LIN x,b,a by AFF_1:6;
then A78: x,b // x,a by AFF_1:def_1;
x <> b by A67, A51, A59, A56, A69, AFF_1:21;
hence contradiction by A67, A51, A61, A68, A66, A69, A70, A78, A77, AFF_1:38; ::_thesis: verum
end;
A79: P // C by A33, A34, AFF_1:44;
A80: x <> c9
proof
A81: now__::_thesis:_not_P_=_Line_(b9,c9)
A82: P // P by A33, AFF_1:44;
assume A83: P = Line (b9,c9) ; ::_thesis: contradiction
then c in P by A39, A40, A79, A63, AFF_1:45;
hence contradiction by A37, A38, A52, A63, A83, A82, AFF_1:39; ::_thesis: verum
end;
assume x = c9 ; ::_thesis: contradiction
then M = Line (b9,c9) by A63, A62, A70, AFF_1:45;
then A84: ( P = Line (b9,c9) or b = b9 ) by A37, A38, A42, A60, A54, A61, AFF_1:18;
then b,a // b,a9 by A46, A81, AFF_1:4;
then LIN b,a,a9 by AFF_1:def_1;
then LIN a,a9,b by AFF_1:6;
then ( b in A or a = a9 ) by A35, A36, A41, AFF_1:25;
then LIN a9,c,c9 by A33, A37, A44, A47, AFF_1:45, AFF_1:def_1;
then LIN c,c9,a9 by AFF_1:6;
then ( c = c9 or a9 in C ) by A39, A40, A43, AFF_1:25;
hence contradiction by A34, A36, A45, A52, A84, A81, AFF_1:2, AFF_1:45; ::_thesis: verum
end;
then Line (x,c9) is being_line by AFF_1:24;
then A // Line (x,c9) by A32, A33, A35, A36, A37, A38, A41, A42, A44, A46, A71, A74, A73, A75, A80, A76, A72, Def12;
then Line (x,c9) // C by A34, AFF_1:44;
then C = Line (x,c9) by A40, A75, AFF_1:45;
then C = Line (a,c) by A39, A43, A52, A67, A59, A69, A71, A73, AFF_1:18;
hence contradiction by A34, A35, A45, A51, AFF_1:45; ::_thesis: verum
end;
theorem :: AFF_2:8
for AP being AffinPlane holds
( AP is satisfying_pap iff AP is satisfying_pap_1 )
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_pap iff AP is satisfying_pap_1 )
hereby ::_thesis: ( AP is satisfying_pap_1 implies AP is satisfying_pap )
assume A1: AP is satisfying_pap ; ::_thesis: AP is satisfying_pap_1
thus AP is satisfying_pap_1 ::_thesis: verum
proof
let M be Subset of AP; :: according to AFF_2:def_14 ::_thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds
c9 in N
let N be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 holds
c9 in N
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & a,b9 // b,a9 & b,c9 // c,b9 & a,c9 // c,a9 & a9 <> b9 implies c9 in N )
assume that
A2: M is being_line and
A3: N is being_line and
A4: a in M and
A5: b in M and
A6: c in M and
A7: M // N and
A8: M <> N and
A9: a9 in N and
A10: b9 in N and
A11: a,b9 // b,a9 and
A12: b,c9 // c,b9 and
A13: a,c9 // c,a9 and
A14: a9 <> b9 ; ::_thesis: c9 in N
A15: c <> a9 by A6, A7, A8, A9, AFF_1:45;
set C = Line (c,b9);
A16: c <> b9 by A6, A7, A8, A10, AFF_1:45;
then Line (c,b9) is being_line by AFF_1:24;
then consider K being Subset of AP such that
A17: b in K and
A18: Line (c,b9) // K by AFF_1:49;
A19: ( c in Line (c,b9) & b9 in Line (c,b9) ) by A16, AFF_1:24;
A20: not K // N
proof
assume K // N ; ::_thesis: contradiction
then Line (c,b9) // N by A18, AFF_1:44;
then Line (c,b9) // M by A7, AFF_1:44;
then b9 in M by A6, A19, AFF_1:45;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
K is being_line by A18, AFF_1:36;
then consider x being Element of AP such that
A21: x in K and
A22: x in N by A3, A20, AFF_1:58;
A23: b,x // c,b9 by A19, A17, A18, A21, AFF_1:39;
then a,x // c,a9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A22, Def13;
then a,x // a,c9 by A13, A15, AFF_1:5;
then LIN a,x,c9 by AFF_1:def_1;
then A24: LIN c9,x,a by AFF_1:6;
A25: a <> b
proof
assume a = b ; ::_thesis: contradiction
then LIN a,b9,a9 by A11, AFF_1:def_1;
then LIN a9,b9,a by AFF_1:6;
then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;
hence contradiction by A4, A7, A8, A14, AFF_1:45; ::_thesis: verum
end;
A26: c9 <> b
proof
assume c9 = b ; ::_thesis: contradiction
then a9 in M by A2, A4, A5, A6, A13, A25, AFF_1:48;
hence contradiction by A7, A8, A9, AFF_1:45; ::_thesis: verum
end;
b,x // b,c9 by A12, A16, A23, AFF_1:5;
then LIN b,x,c9 by AFF_1:def_1;
then A27: LIN c9,x,b by AFF_1:6;
assume A28: not c9 in N ; ::_thesis: contradiction
LIN c9,x,c9 by AFF_1:7;
then c9 in M by A2, A4, A5, A28, A25, A22, A24, A27, AFF_1:8, AFF_1:25;
then b9 in M by A2, A5, A6, A12, A26, AFF_1:48;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
end;
assume A29: AP is satisfying_pap_1 ; ::_thesis: AP is satisfying_pap
let M be Subset of AP; :: according to AFF_2:def_13 ::_thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A30: M is being_line and
A31: N is being_line and
A32: a in M and
A33: b in M and
A34: c in M and
A35: ( M // N & M <> N ) and
A36: a9 in N and
A37: b9 in N and
A38: c9 in N and
A39: a,b9 // b,a9 and
A40: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9
set A = Line (c,a9);
set D = Line (b,c9);
A41: b <> c9 by A33, A35, A38, AFF_1:45;
then A42: ( b in Line (b,c9) & c9 in Line (b,c9) ) by AFF_1:24;
assume A43: not a,c9 // c,a9 ; ::_thesis: contradiction
then A44: c <> a9 by AFF_1:3;
then A45: c in Line (c,a9) by AFF_1:24;
A46: a9 in Line (c,a9) by A44, AFF_1:24;
A47: Line (c,a9) is being_line by A44, AFF_1:24;
then consider P being Subset of AP such that
A48: a in P and
A49: Line (c,a9) // P by AFF_1:49;
A50: a9 <> b9
proof
assume A51: a9 = b9 ; ::_thesis: contradiction
then a9,a // a9,b by A39, AFF_1:4;
then LIN a9,a,b by AFF_1:def_1;
then LIN a,b,a9 by AFF_1:6;
then ( a = b or a9 in M ) by A30, A32, A33, AFF_1:25;
hence contradiction by A35, A36, A40, A43, A51, AFF_1:45; ::_thesis: verum
end;
A52: not Line (b,c9) // P
proof
assume Line (b,c9) // P ; ::_thesis: contradiction
then c,b9 // P by A40, A41, A42, AFF_1:32, AFF_1:40;
then c,b9 // Line (c,a9) by A49, AFF_1:43;
then b9 in Line (c,a9) by A47, A45, AFF_1:23;
then c in N by A31, A36, A37, A50, A47, A45, A46, AFF_1:18;
hence contradiction by A34, A35, AFF_1:45; ::_thesis: verum
end;
A53: Line (b,c9) is being_line by A41, AFF_1:24;
P is being_line by A49, AFF_1:36;
then consider x being Element of AP such that
A54: x in Line (b,c9) and
A55: x in P by A53, A52, AFF_1:58;
LIN b,x,c9 by A53, A42, A54, AFF_1:21;
then b,x // b,c9 by AFF_1:def_1;
then A56: b,x // c,b9 by A40, A41, AFF_1:5;
a,x // c,a9 by A45, A46, A48, A49, A55, AFF_1:39;
then x in N by A29, A30, A31, A32, A33, A34, A35, A36, A37, A39, A50, A56, Def14;
then ( x = c9 or b in N ) by A31, A38, A53, A42, A54, AFF_1:18;
hence contradiction by A33, A35, A43, A45, A46, A48, A49, A55, AFF_1:39, AFF_1:45; ::_thesis: verum
end;
theorem Th9: :: AFF_2:9
for AP being AffinPlane st AP is Pappian holds
AP is satisfying_pap
proof
let AP be AffinPlane; ::_thesis: ( AP is Pappian implies AP is satisfying_pap )
assume A1: AP is Pappian ; ::_thesis: AP is satisfying_pap
let M be Subset of AP; :: according to AFF_2:def_13 ::_thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A2: M is being_line and
A3: N is being_line and
A4: a in M and
A5: b in M and
A6: c in M and
A7: M // N and
A8: M <> N and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9
A14: b <> a9 by A5, A7, A8, A9, AFF_1:45;
set K = Line (a,c9);
set C = Line (c,b9);
A15: c <> b9 by A6, A7, A8, A10, AFF_1:45;
then A16: Line (c,b9) is being_line by AFF_1:24;
assume A17: not a,c9 // c,a9 ; ::_thesis: contradiction
A18: now__::_thesis:_not_a_=_b
assume A19: a = b ; ::_thesis: contradiction
then LIN a,b9,a9 by A12, AFF_1:def_1;
then LIN a9,b9,a by AFF_1:6;
then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;
hence contradiction by A4, A7, A8, A13, A17, A19, AFF_1:45; ::_thesis: verum
end;
A20: now__::_thesis:_not_a9_=_b9
assume a9 = b9 ; ::_thesis: contradiction
then a9,a // a9,b by A12, AFF_1:4;
then LIN a9,a,b by AFF_1:def_1;
then LIN a,b,a9 by AFF_1:6;
then a9 in M by A2, A4, A5, A18, AFF_1:25;
hence contradiction by A7, A8, A9, AFF_1:45; ::_thesis: verum
end;
A21: now__::_thesis:_not_b_=_c
assume A22: b = c ; ::_thesis: contradiction
then LIN b,c9,b9 by A13, AFF_1:def_1;
then LIN b9,c9,b by AFF_1:6;
then ( b9 = c9 or b in N ) by A3, A10, A11, AFF_1:25;
hence contradiction by A5, A7, A8, A12, A17, A22, AFF_1:45; ::_thesis: verum
end;
A23: now__::_thesis:_not_b9_=_c9
assume b9 = c9 ; ::_thesis: contradiction
then b9,b // b9,c by A13, AFF_1:4;
then LIN b9,b,c by AFF_1:def_1;
then LIN b,c,b9 by AFF_1:6;
then b9 in M by A2, A5, A6, A21, AFF_1:25;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
A24: a <> c9 by A4, A7, A8, A11, AFF_1:45;
then A25: a in Line (a,c9) by AFF_1:24;
Line (a,c9) is being_line by A24, AFF_1:24;
then consider T being Subset of AP such that
A26: a9 in T and
A27: Line (a,c9) // T by AFF_1:49;
A28: T is being_line by A27, AFF_1:36;
A29: c9 in Line (a,c9) by A24, AFF_1:24;
A30: ( c in Line (c,b9) & b9 in Line (c,b9) ) by A15, AFF_1:24;
not Line (c,b9) // T
proof
assume Line (c,b9) // T ; ::_thesis: contradiction
then Line (c,b9) // Line (a,c9) by A27, AFF_1:44;
then c,b9 // a,c9 by A25, A29, A30, AFF_1:39;
then b,c9 // a,c9 by A13, A15, AFF_1:5;
then c9,b // c9,a by AFF_1:4;
then LIN c9,b,a by AFF_1:def_1;
then LIN a,b,c9 by AFF_1:6;
then c9 in M by A2, A4, A5, A18, AFF_1:25;
hence contradiction by A7, A8, A11, AFF_1:45; ::_thesis: verum
end;
then consider x being Element of AP such that
A31: x in Line (c,b9) and
A32: x in T by A16, A28, AFF_1:58;
set D = Line (x,b);
A33: x <> b
proof
assume x = b ; ::_thesis: contradiction
then LIN b,c,b9 by A16, A30, A31, AFF_1:21;
then b9 in M by A2, A5, A6, A21, AFF_1:25;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
then A34: b in Line (x,b) by AFF_1:24;
then A35: Line (x,b) <> N by A5, A7, A8, AFF_1:45;
A36: Line (x,b) is being_line by A33, AFF_1:24;
A37: x in Line (x,b) by A33, AFF_1:24;
not Line (x,b) // N
proof
assume Line (x,b) // N ; ::_thesis: contradiction
then Line (x,b) // M by A7, AFF_1:44;
then x in M by A5, A37, A34, AFF_1:45;
then ( c in T or b9 in M ) by A2, A6, A16, A30, A31, A32, AFF_1:18;
hence contradiction by A7, A8, A10, A17, A25, A29, A26, A27, AFF_1:39, AFF_1:45; ::_thesis: verum
end;
then consider o being Element of AP such that
A38: o in Line (x,b) and
A39: o in N by A3, A36, AFF_1:58;
LIN b9,c,x by A16, A30, A31, AFF_1:21;
then A40: b9,c // b9,x by AFF_1:def_1;
A41: a9 <> x
proof
assume a9 = x ; ::_thesis: contradiction
then b9,a9 // b9,c by A40, AFF_1:4;
then LIN b9,a9,c by AFF_1:def_1;
then c in N by A3, A9, A10, A20, AFF_1:25;
hence contradiction by A6, A7, A8, AFF_1:45; ::_thesis: verum
end;
A42: now__::_thesis:_not_o_=_x
assume o = x ; ::_thesis: contradiction
then N = T by A3, A9, A26, A28, A32, A39, A41, AFF_1:18;
then N = Line (a,c9) by A11, A29, A27, AFF_1:45;
hence contradiction by A4, A7, A8, A25, AFF_1:45; ::_thesis: verum
end;
A43: a,c9 // x,a9 by A25, A29, A26, A27, A32, AFF_1:39;
A44: now__::_thesis:_not_o_=_a9
assume o = a9 ; ::_thesis: contradiction
then LIN a9,b,x by A36, A37, A34, A38, AFF_1:21;
then a9,b // a9,x by AFF_1:def_1;
then b,a9 // x,a9 by AFF_1:4;
then a,b9 // x,a9 by A12, A14, AFF_1:5;
then a,b9 // a,c9 by A43, A41, AFF_1:5;
then LIN a,b9,c9 by AFF_1:def_1;
then LIN b9,c9,a by AFF_1:6;
then a in N by A3, A10, A11, A23, AFF_1:25;
hence contradiction by A4, A7, A8, AFF_1:45; ::_thesis: verum
end;
c,b9 // x,b9 by A40, AFF_1:4;
then A45: b,c9 // x,b9 by A13, A15, AFF_1:5;
A46: a <> b9 by A4, A7, A8, A10, AFF_1:45;
not a,b9 // Line (x,b)
proof
assume a,b9 // Line (x,b) ; ::_thesis: contradiction
then b,a9 // Line (x,b) by A12, A46, AFF_1:32;
then a9 in Line (x,b) by A36, A34, AFF_1:23;
then b in T by A26, A28, A32, A36, A37, A34, A41, AFF_1:18;
then b,a9 // a,c9 by A25, A29, A26, A27, AFF_1:39;
then a,b9 // a,c9 by A12, A14, AFF_1:5;
then LIN a,b9,c9 by AFF_1:def_1;
then LIN b9,c9,a by AFF_1:6;
then a in N by A3, A10, A11, A23, AFF_1:25;
hence contradiction by A4, A7, A8, AFF_1:45; ::_thesis: verum
end;
then consider y being Element of AP such that
A47: y in Line (x,b) and
A48: LIN a,b9,y by A36, AFF_1:59;
A49: LIN a,y,a by AFF_1:7;
A50: b9 <> x
proof
assume b9 = x ; ::_thesis: contradiction
then a,c9 // a9,b9 by A25, A29, A26, A27, A32, AFF_1:39;
then a,c9 // N by A3, A9, A10, A20, AFF_1:27;
then c9,a // N by AFF_1:34;
then a in N by A3, A11, AFF_1:23;
hence contradiction by A4, A7, A8, AFF_1:45; ::_thesis: verum
end;
A51: now__::_thesis:_not_o_=_b9
assume o = b9 ; ::_thesis: contradiction
then LIN b9,x,b by A36, A37, A34, A38, AFF_1:21;
then b9,x // b9,b by AFF_1:def_1;
then x,b9 // b,b9 by AFF_1:4;
then b,c9 // b,b9 by A45, A50, AFF_1:5;
then LIN b,c9,b9 by AFF_1:def_1;
then LIN b9,c9,b by AFF_1:6;
then b in N by A3, A10, A11, A23, AFF_1:25;
hence contradiction by A5, A7, A8, AFF_1:45; ::_thesis: verum
end;
A52: now__::_thesis:_not_o_=_y
assume o = y ; ::_thesis: contradiction
then LIN b9,o,a by A48, AFF_1:6;
then a in N by A3, A10, A39, A51, AFF_1:25;
hence contradiction by A4, A7, A8, AFF_1:45; ::_thesis: verum
end;
A53: b <> c9 by A5, A7, A8, A11, AFF_1:45;
A54: now__::_thesis:_not_o_=_c9
assume o = c9 ; ::_thesis: contradiction
then Line (x,b) // Line (c,b9) by A13, A15, A53, A16, A30, A36, A34, A38, AFF_1:38;
then b in Line (c,b9) by A31, A37, A34, AFF_1:45;
then LIN c,b,b9 by A16, A30, AFF_1:21;
then b9 in M by A2, A5, A6, A21, AFF_1:25;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
LIN b9,a,y by A48, AFF_1:6;
then b9,a // b9,y by AFF_1:def_1;
then a,b9 // y,b9 by AFF_1:4;
then A55: y,b9 // b,a9 by A12, A46, AFF_1:5;
o <> b by A5, A7, A8, A39, AFF_1:45;
then y,c9 // x,a9 by A1, A3, A9, A10, A11, A36, A37, A34, A38, A39, A45, A47, A55, A35, A51, A44, A54, A42, A52, Def2;
then y,c9 // a,c9 by A43, A41, AFF_1:5;
then c9,y // c9,a by AFF_1:4;
then LIN c9,y,a by AFF_1:def_1;
then A56: LIN a,y,c9 by AFF_1:6;
LIN a,y,b9 by A48, AFF_1:6;
then ( a in Line (x,b) or a in N ) by A3, A10, A11, A23, A47, A56, A49, AFF_1:8, AFF_1:25;
then Line (x,b) // N by A2, A4, A5, A7, A8, A18, A36, A34, AFF_1:18, AFF_1:45;
hence contradiction by A38, A39, A35, AFF_1:45; ::_thesis: verum
end;
theorem Th10: :: AFF_2:10
for AP being AffinPlane holds
( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) )
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) )
A1: ( AP is Pappian & AP is satisfying_pap implies AP is satisfying_PPAP )
proof
assume that
A2: AP is Pappian and
A3: AP is satisfying_pap ; ::_thesis: AP is satisfying_PPAP
thus AP is satisfying_PPAP ::_thesis: verum
proof
let M be Subset of AP; :: according to AFF_2:def_1 ::_thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A4: M is being_line and
A5: N is being_line and
A6: a in M and
A7: b in M and
A8: c in M and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9
now__::_thesis:_(_M_<>_N_&_not_a,c9_//_c,a9_implies_a,c9_//_c,a9_)
assume A14: M <> N ; ::_thesis: ( not a,c9 // c,a9 implies a,c9 // c,a9 )
assume A15: not a,c9 // c,a9 ; ::_thesis: a,c9 // c,a9
now__::_thesis:_(_not_M_//_N_implies_a,c9_//_c,a9_)
assume not M // N ; ::_thesis: a,c9 // c,a9
then consider o being Element of AP such that
A16: o in M and
A17: o in N by A4, A5, AFF_1:58;
A18: o <> a
proof
assume A19: o = a ; ::_thesis: contradiction
then o,b9 // a9,b by A12, AFF_1:4;
then ( o = b9 or b in N ) by A5, A9, A10, A17, AFF_1:48;
then ( o = b9 or o = b ) by A4, A5, A7, A14, A16, A17, AFF_1:18;
then ( c,o // b,c9 or o,c9 // b9,c ) by A13, AFF_1:4;
then ( c9 in M or c = o or c in N or o = c9 ) by A4, A5, A7, A8, A10, A11, A16, A17, AFF_1:48;
then ( o = c or o = c9 ) by A4, A5, A8, A11, A14, A16, A17, AFF_1:18;
hence contradiction by A5, A9, A11, A15, A17, A19, AFF_1:3, AFF_1:51; ::_thesis: verum
end;
A20: o <> b
proof
assume A21: o = b ; ::_thesis: contradiction
then o,c9 // b9,c by A13, AFF_1:4;
then ( o = c9 or c in N ) by A5, A10, A11, A17, AFF_1:48;
then A22: ( o = c9 or o = c ) by A4, A5, A8, A14, A16, A17, AFF_1:18;
o,a9 // b9,a by A12, A21, AFF_1:4;
then ( o = a9 or a in N ) by A5, A9, A10, A17, AFF_1:48;
hence contradiction by A4, A5, A6, A8, A14, A15, A16, A17, A18, A22, AFF_1:3, AFF_1:18, AFF_1:51; ::_thesis: verum
end;
A23: o <> c9
proof
assume A24: o = c9 ; ::_thesis: contradiction
then b9 in M by A4, A7, A8, A13, A16, A20, AFF_1:48;
then a,o // b,a9 by A4, A5, A10, A12, A14, A16, A17, AFF_1:18;
then a9 in M by A4, A6, A7, A16, A18, AFF_1:48;
hence contradiction by A4, A6, A8, A15, A16, A24, AFF_1:51; ::_thesis: verum
end;
A25: o <> c
proof
assume A26: o = c ; ::_thesis: contradiction
then o,b9 // c9,b by A13, AFF_1:4;
then ( o = b9 or b in N ) by A5, A10, A11, A17, AFF_1:48;
then a9 in M by A4, A5, A6, A7, A9, A12, A16, A17, A18, A20, AFF_1:18, AFF_1:48;
then a9 = o by A4, A5, A9, A14, A16, A17, AFF_1:18;
hence contradiction by A15, A26, AFF_1:3; ::_thesis: verum
end;
A27: o <> a9
proof
assume A28: o = a9 ; ::_thesis: contradiction
then o,b // a,b9 by A12, AFF_1:4;
then b9 in M by A4, A6, A7, A16, A20, AFF_1:48;
then o = b9 by A4, A5, A10, A14, A16, A17, AFF_1:18;
then c,o // b,c9 by A13, AFF_1:4;
then c9 in M by A4, A7, A8, A16, A25, AFF_1:48;
hence contradiction by A4, A6, A8, A15, A16, A28, AFF_1:51; ::_thesis: verum
end;
o <> b9
proof
assume A29: o = b9 ; ::_thesis: contradiction
then o,c // b,c9 by A13, AFF_1:4;
then A30: c9 in M by A4, A7, A8, A16, A25, AFF_1:48;
a9 in M by A4, A6, A7, A12, A16, A18, A29, AFF_1:48;
hence contradiction by A4, A6, A8, A15, A30, AFF_1:51; ::_thesis: verum
end;
hence a,c9 // c,a9 by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A16, A17, A18, A20, A25, A27, A23, Def2; ::_thesis: verum
end;
hence a,c9 // c,a9 by A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Def13; ::_thesis: verum
end;
hence a,c9 // c,a9 by A4, A6, A8, A9, A11, AFF_1:51; ::_thesis: verum
end;
end;
( AP is satisfying_PPAP implies ( AP is Pappian & AP is satisfying_pap ) )
proof
assume A31: AP is satisfying_PPAP ; ::_thesis: ( AP is Pappian & AP is satisfying_pap )
thus AP is Pappian ::_thesis: AP is satisfying_pap
proof
let M be Subset of AP; :: according to AFF_2:def_2 ::_thesis: for N being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A32: ( M is being_line & N is being_line ) and
( M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 ) and
A33: ( a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 ) ; ::_thesis: a,c9 // c,a9
thus a,c9 // c,a9 by A31, A32, A33, Def1; ::_thesis: verum
end;
thus AP is satisfying_pap ::_thesis: verum
proof
let M be Subset of AP; :: according to AFF_2:def_13 ::_thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A34: ( M is being_line & N is being_line & a in M & b in M & c in M ) and
( M // N & M <> N ) and
A35: ( a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 ) ; ::_thesis: a,c9 // c,a9
thus a,c9 // c,a9 by A31, A34, A35, Def1; ::_thesis: verum
end;
end;
hence ( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) ) by A1; ::_thesis: verum
end;
theorem :: AFF_2:11
for AP being AffinPlane st AP is Pappian holds
AP is Desarguesian
proof
let AP be AffinPlane; ::_thesis: ( AP is Pappian implies AP is Desarguesian )
assume A1: AP is Pappian ; ::_thesis: AP is Desarguesian
then AP is satisfying_pap by Th9;
then A2: AP is satisfying_PPAP by A1, Th10;
let A be Subset of AP; :: according to AFF_2:def_4 ::_thesis: for P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let P, C be Subset of AP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A3: o in A and
A4: o in P and
A5: o in C and
A6: o <> a and
A7: o <> b and
o <> c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A <> P and
A18: A <> C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
assume A21: not b,c // b9,c9 ; ::_thesis: contradiction
then A22: b <> c by AFF_1:3;
A23: a <> c by A3, A5, A6, A8, A12, A14, A16, A18, AFF_1:18;
A24: not b in C
proof
assume A25: b in C ; ::_thesis: contradiction
then b9 in C by A4, A5, A7, A10, A11, A15, A16, AFF_1:18;
hence contradiction by A12, A13, A16, A21, A25, AFF_1:51; ::_thesis: verum
end;
A26: a <> b by A3, A4, A6, A8, A10, A14, A15, A17, AFF_1:18;
A27: a <> a9
proof
assume A28: a = a9 ; ::_thesis: contradiction
then LIN a,c,c9 by A20, AFF_1:def_1;
then LIN c,c9,a by AFF_1:6;
then A29: ( c = c9 or a in C ) by A12, A13, A16, AFF_1:25;
LIN a,b,b9 by A19, A28, AFF_1:def_1;
then LIN b,b9,a by AFF_1:6;
then ( b = b9 or a in P ) by A10, A11, A15, AFF_1:25;
hence contradiction by A3, A4, A5, A6, A8, A14, A15, A16, A17, A18, A21, A29, AFF_1:2, AFF_1:18; ::_thesis: verum
end;
set M = Line (b9,c9);
set N = Line (a9,b9);
set D = Line (a9,c9);
A30: a9 <> b9
proof
A31: a9,c9 // c,a by A20, AFF_1:4;
assume A32: a9 = b9 ; ::_thesis: contradiction
then a9 in C by A3, A4, A5, A9, A11, A14, A15, A17, AFF_1:18;
then ( a in C or a9 = c9 ) by A12, A13, A16, A31, AFF_1:48;
hence contradiction by A3, A5, A6, A8, A14, A16, A18, A21, A32, AFF_1:3, AFF_1:18; ::_thesis: verum
end;
then A33: Line (a9,b9) is being_line by AFF_1:24;
A34: a9 <> c9
proof
assume a9 = c9 ; ::_thesis: contradiction
then A35: a9 in P by A3, A4, A5, A9, A13, A14, A16, A18, AFF_1:18;
a9,b9 // b,a by A19, AFF_1:4;
then a in P by A10, A11, A15, A30, A35, AFF_1:48;
hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:18; ::_thesis: verum
end;
A36: not LIN a9,b9,c9
proof
assume A37: LIN a9,b9,c9 ; ::_thesis: contradiction
then a9,b9 // a9,c9 by AFF_1:def_1;
then a9,b9 // a,c by A20, A34, AFF_1:5;
then a,b // a,c by A19, A30, AFF_1:5;
then LIN a,b,c by AFF_1:def_1;
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def_1;
then b,c // a,b by AFF_1:4;
then A38: b,c // a9,b9 by A19, A26, AFF_1:5;
LIN b9,c9,a9 by A37, AFF_1:6;
then b9,c9 // b9,a9 by AFF_1:def_1;
then b9,c9 // a9,b9 by AFF_1:4;
hence contradiction by A21, A30, A38, AFF_1:5; ::_thesis: verum
end;
A39: not LIN a,b,c
proof
assume LIN a,b,c ; ::_thesis: contradiction
then a,b // a,c by AFF_1:def_1;
then a,b // a9,c9 by A20, A23, AFF_1:5;
then a9,b9 // a9,c9 by A19, A26, AFF_1:5;
hence contradiction by A36, AFF_1:def_1; ::_thesis: verum
end;
A40: now__::_thesis:_b,c_//_A
LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;
then o,a // o,a9 by AFF_1:def_1;
then A41: a9,o // a,o by AFF_1:4;
set M = Line (b,c);
set N = Line (a,b);
set D = Line (a,c);
A42: Line (a,b) is being_line by A26, AFF_1:24;
Line (b,c) is being_line by A22, AFF_1:24;
then consider K being Subset of AP such that
A43: o in K and
A44: Line (b,c) // K by AFF_1:49;
A45: K is being_line by A44, AFF_1:36;
A46: a in Line (a,b) by A26, AFF_1:24;
A47: b in Line (a,b) by A26, AFF_1:24;
A48: ( b in Line (b,c) & c in Line (b,c) ) by A22, AFF_1:24;
not Line (a,b) // K
proof
assume Line (a,b) // K ; ::_thesis: contradiction
then Line (a,b) // Line (b,c) by A44, AFF_1:44;
then c in Line (a,b) by A48, A47, AFF_1:45;
hence contradiction by A39, A42, A46, A47, AFF_1:21; ::_thesis: verum
end;
then consider p being Element of AP such that
A49: p in Line (a,b) and
A50: p in K by A42, A45, AFF_1:58;
A51: b,c // p,o by A48, A43, A44, A50, AFF_1:39;
A52: o <> p
proof
assume o = p ; ::_thesis: contradiction
then LIN o,a,b by A42, A46, A47, A49, AFF_1:21;
then b in A by A3, A6, A8, A14, AFF_1:25;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; ::_thesis: verum
end;
set R = Line (a9,p);
A53: p <> a9
proof
assume p = a9 ; ::_thesis: contradiction
then b in A by A8, A9, A14, A27, A42, A46, A47, A49, AFF_1:18;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; ::_thesis: verum
end;
then A54: Line (a9,p) is being_line by AFF_1:24;
Line (a,c) is being_line by A23, AFF_1:24;
then consider T being Subset of AP such that
A55: p in T and
A56: Line (a,c) // T by AFF_1:49;
A57: ( a in Line (a,c) & c in Line (a,c) ) by A23, AFF_1:24;
A58: not C // T
proof
assume C // T ; ::_thesis: contradiction
then C // Line (a,c) by A56, AFF_1:44;
then a in C by A12, A57, AFF_1:45;
hence contradiction by A3, A5, A6, A8, A14, A16, A18, AFF_1:18; ::_thesis: verum
end;
T is being_line by A56, AFF_1:36;
then consider q being Element of AP such that
A59: q in C and
A60: q in T by A16, A58, AFF_1:58;
A61: p,q // a,c by A57, A55, A56, A60, AFF_1:39;
then A62: b,q // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, Def1;
A63: ( a9 in Line (a9,p) & p in Line (a9,p) ) by A53, AFF_1:24;
assume not b,c // A ; ::_thesis: contradiction
then A64: K <> A by A48, A44, AFF_1:40;
not b,q // Line (a9,p)
proof
assume b,q // Line (a9,p) ; ::_thesis: contradiction
then A65: a,o // Line (a9,p) by A24, A59, A62, AFF_1:32;
a,o // A by A3, A8, A14, AFF_1:40, AFF_1:41;
then p in A by A6, A9, A63, A65, AFF_1:45, AFF_1:53;
hence contradiction by A3, A14, A43, A45, A50, A52, A64, AFF_1:18; ::_thesis: verum
end;
then consider r being Element of AP such that
A66: r in Line (a9,p) and
A67: LIN b,q,r by A54, AFF_1:59;
A68: now__::_thesis:_(_r_=_q_implies_r,b_//_o,a9_)
assume r = q ; ::_thesis: r,b // o,a9
then b,r // a,o by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, A61, Def1;
then A69: r,b // o,a by AFF_1:4;
LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;
then o,a // o,a9 by AFF_1:def_1;
hence r,b // o,a9 by A6, A69, AFF_1:5; ::_thesis: verum
end;
LIN q,r,b by A67, AFF_1:6;
then q,r // q,b by AFF_1:def_1;
then r,q // b,q by AFF_1:4;
then r,q // a,o by A24, A59, A62, AFF_1:5;
then A70: a9,o // r,q by A6, A41, AFF_1:5;
LIN b,a,p by A42, A46, A47, A49, AFF_1:21;
then b,a // b,p by AFF_1:def_1;
then a,b // p,b by AFF_1:4;
then A71: p,b // a9,b9 by A19, A26, AFF_1:5;
LIN r,b,q by A67, AFF_1:6;
then r,b // r,q by AFF_1:def_1;
then a9,o // r,b by A70, A68, AFF_1:4, AFF_1:5;
then A72: p,o // r,b9 by A2, A4, A10, A11, A15, A54, A63, A66, A71, Def1;
p,q // a9,c9 by A20, A23, A61, AFF_1:5;
then A73: p,o // r,c9 by A2, A5, A13, A16, A59, A54, A63, A66, A70, Def1;
then r,c9 // r,b9 by A52, A72, AFF_1:5;
then LIN r,c9,b9 by AFF_1:def_1;
then LIN c9,b9,r by AFF_1:6;
then c9,b9 // c9,r by AFF_1:def_1;
then A74: r,c9 // b9,c9 by AFF_1:4;
b,c // r,c9 by A52, A51, A73, AFF_1:5;
then r = c9 by A21, A74, AFF_1:5;
then p,o // b9,c9 by A72, AFF_1:4;
hence contradiction by A21, A52, A51, AFF_1:5; ::_thesis: verum
end;
A75: b9 in Line (a9,b9) by A30, AFF_1:24;
A76: b9 <> c9 by A21, AFF_1:3;
then A77: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:24;
Line (b9,c9) is being_line by A76, AFF_1:24;
then consider K being Subset of AP such that
A78: o in K and
A79: Line (b9,c9) // K by AFF_1:49;
A80: K is being_line by A79, AFF_1:36;
A81: a9 in Line (a9,b9) by A30, AFF_1:24;
not Line (a9,b9) // K
proof
assume Line (a9,b9) // K ; ::_thesis: contradiction
then Line (a9,b9) // Line (b9,c9) by A79, AFF_1:44;
then c9 in Line (a9,b9) by A77, A75, AFF_1:45;
hence contradiction by A36, A33, A81, A75, AFF_1:21; ::_thesis: verum
end;
then consider p being Element of AP such that
A82: p in Line (a9,b9) and
A83: p in K by A33, A80, AFF_1:58;
A84: o <> a9
proof
assume A85: o = a9 ; ::_thesis: contradiction
a9,b9 // b,a by A19, AFF_1:4;
then a in P by A4, A10, A11, A15, A30, A85, AFF_1:48;
hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1:18; ::_thesis: verum
end;
A86: o <> p
proof
assume o = p ; ::_thesis: contradiction
then LIN o,a9,b9 by A33, A81, A75, A82, AFF_1:21;
then A87: b9 in A by A3, A9, A14, A84, AFF_1:25;
a9,b9 // a,b by A19, AFF_1:4;
then b in A by A8, A9, A14, A30, A87, AFF_1:48;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; ::_thesis: verum
end;
Line (a9,c9) is being_line by A34, AFF_1:24;
then consider T being Subset of AP such that
A88: p in T and
A89: Line (a9,c9) // T by AFF_1:49;
A90: T is being_line by A89, AFF_1:36;
A91: ( a9 in Line (a9,c9) & c9 in Line (a9,c9) ) by A34, AFF_1:24;
not C // T
proof
assume C // T ; ::_thesis: contradiction
then C // Line (a9,c9) by A89, AFF_1:44;
then a9 in C by A13, A91, AFF_1:45;
hence contradiction by A3, A5, A9, A14, A16, A18, A84, AFF_1:18; ::_thesis: verum
end;
then consider q being Element of AP such that
A92: q in C and
A93: q in T by A16, A90, AFF_1:58;
A94: b9,c9 // p,o by A77, A78, A79, A83, AFF_1:39;
A95: o <> b9
proof
assume A96: o = b9 ; ::_thesis: contradiction
b9,a9 // a,b by A19, AFF_1:4;
then b in A by A3, A8, A9, A14, A30, A96, AFF_1:48;
hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1:18; ::_thesis: verum
end;
A97: b9 <> q
proof
assume b9 = q ; ::_thesis: contradiction
then P = C by A4, A5, A11, A15, A16, A95, A92, AFF_1:18;
hence contradiction by A10, A11, A12, A13, A15, A21, AFF_1:51; ::_thesis: verum
end;
set R = Line (a,p);
A98: p <> a
proof
assume p = a ; ::_thesis: contradiction
then b9 in A by A8, A9, A14, A27, A33, A81, A75, A82, AFF_1:18;
hence contradiction by A3, A4, A11, A14, A15, A17, A95, AFF_1:18; ::_thesis: verum
end;
then A99: Line (a,p) is being_line by AFF_1:24;
A100: p,q // a9,c9 by A91, A88, A89, A93, AFF_1:39;
then A101: b9,q // a9,o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, Def1;
A102: ( a in Line (a,p) & p in Line (a,p) ) by A98, AFF_1:24;
not b9,c9 // A by A14, A21, A40, AFF_1:31;
then A103: K <> A by A77, A79, AFF_1:40;
not b9,q // Line (a,p)
proof
assume b9,q // Line (a,p) ; ::_thesis: contradiction
then A104: a9,o // Line (a,p) by A101, A97, AFF_1:32;
a9,o // A by A3, A9, A14, AFF_1:40, AFF_1:41;
then p in A by A8, A84, A102, A104, AFF_1:45, AFF_1:53;
hence contradiction by A3, A14, A78, A80, A83, A86, A103, AFF_1:18; ::_thesis: verum
end;
then consider r being Element of AP such that
A105: r in Line (a,p) and
A106: LIN b9,q,r by A99, AFF_1:59;
A107: now__::_thesis:_(_r_=_q_implies_r,b9_//_o,a_)
assume r = q ; ::_thesis: r,b9 // o,a
then b9,r // a9,o by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, A100, Def1;
then A108: r,b9 // o,a9 by AFF_1:4;
LIN o,a9,a by A3, A8, A9, A14, AFF_1:21;
then o,a9 // o,a by AFF_1:def_1;
hence r,b9 // o,a by A84, A108, AFF_1:5; ::_thesis: verum
end;
LIN b9,a9,p by A33, A81, A75, A82, AFF_1:21;
then b9,a9 // b9,p by AFF_1:def_1;
then p,b9 // a9,b9 by AFF_1:4;
then A109: p,b9 // a,b by A19, A30, AFF_1:5;
LIN o,a,a9 by A3, A8, A9, A14, AFF_1:21;
then o,a // o,a9 by AFF_1:def_1;
then A110: a,o // a9,o by AFF_1:4;
LIN q,r,b9 by A106, AFF_1:6;
then q,r // q,b9 by AFF_1:def_1;
then r,q // b9,q by AFF_1:4;
then r,q // a9,o by A101, A97, AFF_1:5;
then A111: a,o // r,q by A84, A110, AFF_1:5;
LIN r,b9,q by A106, AFF_1:6;
then r,b9 // r,q by AFF_1:def_1;
then a,o // r,b9 by A111, A107, AFF_1:4, AFF_1:5;
then A112: p,o // r,b by A2, A4, A10, A11, A15, A99, A102, A105, A109, Def1;
p,q // a,c by A20, A34, A100, AFF_1:5;
then A113: p,o // r,c by A2, A5, A12, A16, A92, A99, A102, A105, A111, Def1;
then r,c // r,b by A86, A112, AFF_1:5;
then LIN r,c,b by AFF_1:def_1;
then LIN c,b,r by AFF_1:6;
then c,b // c,r by AFF_1:def_1;
then A114: b,c // r,c by AFF_1:4;
b9,c9 // r,c by A86, A94, A113, AFF_1:5;
then r = c by A21, A114, AFF_1:5;
then b,c // p,o by A112, AFF_1:4;
hence contradiction by A21, A86, A94, AFF_1:5; ::_thesis: verum
end;
theorem :: AFF_2:12
for AP being AffinPlane st AP is Desarguesian holds
AP is Moufangian
proof
let AP be AffinPlane; ::_thesis: ( AP is Desarguesian implies AP is Moufangian )
assume A1: AP is Desarguesian ; ::_thesis: AP is Moufangian
let K be Subset of AP; :: according to AFF_2:def_7 ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )
assume that
A2: K is being_line and
A3: o in K and
A4: ( c in K & c9 in K ) and
A5: not a in K and
A6: o <> c and
A7: a <> b and
A8: LIN o,a,a9 and
A9: LIN o,b,b9 and
A10: ( a,b // a9,b9 & a,c // a9,c9 ) and
A11: a,b // K ; ::_thesis: b,c // b9,c9
set A = Line (o,a);
set P = Line (o,b);
A12: o in Line (o,a) by A3, A5, AFF_1:24;
A13: now__::_thesis:_not_o_=_b
assume A14: o = b ; ::_thesis: contradiction
b,a // K by A11, AFF_1:34;
hence contradiction by A2, A3, A5, A14, AFF_1:23; ::_thesis: verum
end;
then A15: b in Line (o,b) by AFF_1:24;
A16: a in Line (o,a) by A3, A5, AFF_1:24;
A17: Line (o,a) is being_line by A3, A5, AFF_1:24;
A18: Line (o,a) <> Line (o,b)
proof
assume Line (o,a) = Line (o,b) ; ::_thesis: contradiction
then a,b // Line (o,a) by A17, A16, A15, AFF_1:40, AFF_1:41;
hence contradiction by A3, A5, A7, A11, A12, A16, AFF_1:45, AFF_1:53; ::_thesis: verum
end;
A19: ( Line (o,b) is being_line & o in Line (o,b) ) by A13, AFF_1:24;
then A20: b9 in Line (o,b) by A9, A13, A15, AFF_1:25;
a9 in Line (o,a) by A3, A5, A8, A17, A12, A16, AFF_1:25;
hence b,c // b9,c9 by A1, A2, A3, A4, A5, A6, A10, A13, A17, A12, A16, A19, A15, A20, A18, Def4; ::_thesis: verum
end;
theorem Th13: :: AFF_2:13
for AP being AffinPlane st AP is satisfying_TDES_1 holds
AP is satisfying_des_1
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_TDES_1 implies AP is satisfying_des_1 )
assume A1: AP is satisfying_TDES_1 ; ::_thesis: AP is satisfying_des_1
let A be Subset of AP; :: according to AFF_2:def_12 ::_thesis: for P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let P, C be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies A // C )
assume that
A2: A // P and
A3: a in A and
A4: a9 in A and
A5: b in P and
A6: b9 in P and
A7: c in C and
A8: c9 in C and
A9: A is being_line and
A10: P is being_line and
A11: C is being_line and
A12: A <> P and
A13: A <> C and
A14: a,b // a9,b9 and
A15: a,c // a9,c9 and
A16: b,c // b9,c9 and
A17: not LIN a,b,c and
A18: c <> c9 ; ::_thesis: A // C
set P9 = Line (a,b);
set C9 = Line (a9,b9);
A19: a9 <> b9 by A2, A4, A6, A12, AFF_1:45;
then A20: a9 in Line (a9,b9) by AFF_1:24;
A21: a9 <> c9
proof
assume a9 = c9 ; ::_thesis: contradiction
then b,c // a9,b9 by A16, AFF_1:4;
then a,b // b,c by A14, A19, AFF_1:5;
then b,a // b,c by AFF_1:4;
then LIN b,a,c by AFF_1:def_1;
hence contradiction by A17, AFF_1:6; ::_thesis: verum
end;
A22: not c9 in A
proof
assume A23: c9 in A ; ::_thesis: contradiction
a9,c9 // a,c by A15, AFF_1:4;
then c in A by A3, A4, A9, A21, A23, AFF_1:48;
hence contradiction by A7, A8, A9, A11, A13, A18, A23, AFF_1:18; ::_thesis: verum
end;
A24: Line (a9,b9) is being_line by A19, AFF_1:24;
assume A25: not A // C ; ::_thesis: contradiction
then consider o being Element of AP such that
A26: o in A and
A27: o in C by A9, A11, AFF_1:58;
A28: LIN o,c9,c by A7, A8, A11, A27, AFF_1:21;
A29: a <> a9
proof
assume A30: a = a9 ; ::_thesis: contradiction
then LIN a,c,c9 by A15, AFF_1:def_1;
then A31: LIN c,c9,a by AFF_1:6;
LIN a,b,b9 by A14, A30, AFF_1:def_1;
then LIN b,b9,a by AFF_1:6;
then ( b = b9 or a in P ) by A5, A6, A10, AFF_1:25;
then LIN b,c,c9 by A2, A3, A12, A16, AFF_1:45, AFF_1:def_1;
then A32: LIN c,c9,b by AFF_1:6;
LIN c,c9,c by AFF_1:7;
hence contradiction by A17, A18, A31, A32, AFF_1:8; ::_thesis: verum
end;
A33: o <> a9
proof
assume A34: o = a9 ; ::_thesis: contradiction
a9,c9 // c,a by A15, AFF_1:4;
then a in C by A7, A8, A11, A27, A21, A34, AFF_1:48;
hence contradiction by A3, A4, A9, A11, A13, A27, A29, A34, AFF_1:18; ::_thesis: verum
end;
A35: a <> b by A17, AFF_1:7;
then A36: Line (a,b) is being_line by AFF_1:24;
consider N being Subset of AP such that
A37: c9 in N and
A38: A // N by A9, AFF_1:49;
A39: b9 in Line (a9,b9) by A19, AFF_1:24;
A40: not N // Line (a9,b9)
proof
assume N // Line (a9,b9) ; ::_thesis: contradiction
then A // Line (a9,b9) by A38, AFF_1:44;
then b9 in A by A4, A39, A20, AFF_1:45;
hence contradiction by A2, A6, A12, AFF_1:45; ::_thesis: verum
end;
N is being_line by A38, AFF_1:36;
then consider q being Element of AP such that
A41: q in N and
A42: q in Line (a9,b9) by A24, A40, AFF_1:58;
A43: c9,q // A by A37, A38, A41, AFF_1:40;
A44: c9 <> q
proof
assume c9 = q ; ::_thesis: contradiction
then LIN a9,b9,c9 by A24, A39, A20, A42, AFF_1:21;
then a9,b9 // a9,c9 by AFF_1:def_1;
then a9,b9 // a,c by A15, A21, AFF_1:5;
then a,b // a,c by A14, A19, AFF_1:5;
hence contradiction by A17, AFF_1:def_1; ::_thesis: verum
end;
A45: c9,a9 // c,a by A15, AFF_1:4;
A46: c,b // c9,b9 by A16, AFF_1:4;
A47: a in Line (a,b) by A35, AFF_1:24;
A48: b <> c by A17, AFF_1:7;
A49: not c in P
proof
assume A50: c in P ; ::_thesis: contradiction
then c9 in P by A5, A6, A10, A16, A48, AFF_1:48;
hence contradiction by A2, A7, A8, A10, A11, A18, A25, A50, AFF_1:18; ::_thesis: verum
end;
not P // C by A2, A25, AFF_1:44;
then consider s being Element of AP such that
A51: s in P and
A52: s in C by A10, A11, AFF_1:58;
A53: LIN s,c,c9 by A7, A8, A11, A52, AFF_1:21;
A54: b <> b9
proof
assume b = b9 ; ::_thesis: contradiction
then b,a // b,a9 by A14, AFF_1:4;
then LIN b,a,a9 by AFF_1:def_1;
then LIN a,a9,b by AFF_1:6;
then b in A by A3, A4, A9, A29, AFF_1:25;
hence contradiction by A2, A5, A12, AFF_1:45; ::_thesis: verum
end;
A55: s <> b
proof
assume A56: s = b ; ::_thesis: contradiction
b,c // c9,b9 by A16, AFF_1:4;
then b9 in C by A7, A8, A11, A48, A52, A56, AFF_1:48;
hence contradiction by A2, A5, A6, A10, A11, A25, A54, A52, A56, AFF_1:18; ::_thesis: verum
end;
consider M being Subset of AP such that
A57: c in M and
A58: A // M by A9, AFF_1:49;
A59: M is being_line by A58, AFF_1:36;
A60: b in Line (a,b) by A35, AFF_1:24;
not M // Line (a,b)
proof
assume M // Line (a,b) ; ::_thesis: contradiction
then A // Line (a,b) by A58, AFF_1:44;
then b in A by A3, A60, A47, AFF_1:45;
hence contradiction by A2, A5, A12, AFF_1:45; ::_thesis: verum
end;
then consider p being Element of AP such that
A61: p in M and
A62: p in Line (a,b) by A59, A36, AFF_1:58;
M // P by A2, A58, AFF_1:44;
then A63: c,p // P by A57, A61, AFF_1:40;
A64: M // N by A58, A38, AFF_1:44;
then A65: c,p // c9,q by A57, A37, A61, A41, AFF_1:39;
A66: now__::_thesis:_not_p_=_q
assume p = q ; ::_thesis: contradiction
then M = N by A64, A61, A41, AFF_1:45;
hence contradiction by A7, A8, A11, A18, A25, A57, A58, A37, A59, AFF_1:18; ::_thesis: verum
end;
A67: Line (a,b) // Line (a9,b9) by A14, A35, A19, AFF_1:37;
then A68: p,b // q,b9 by A60, A39, A62, A42, AFF_1:39;
A69: q,a9 // p,a by A47, A20, A67, A62, A42, AFF_1:39;
c9,q // c,p by A57, A37, A64, A61, A41, AFF_1:39;
then LIN o,q,p by A1, A3, A4, A9, A26, A28, A22, A45, A69, A43, A44, A33, Def8;
then A70: LIN p,q,o by AFF_1:6;
c <> p by A17, A36, A60, A47, A62, AFF_1:21;
then LIN s,p,q by A1, A5, A6, A10, A51, A53, A63, A68, A49, A55, A65, A46, Def8;
then A71: LIN p,q,s by AFF_1:6;
LIN p,q,p by AFF_1:7;
then ( o = s or p in C ) by A11, A27, A52, A70, A71, A66, AFF_1:8, AFF_1:25;
then c in Line (a,b) by A2, A7, A11, A12, A25, A26, A57, A58, A59, A61, A62, A51, AFF_1:18, AFF_1:45;
hence contradiction by A17, A36, A60, A47, AFF_1:21; ::_thesis: verum
end;
theorem :: AFF_2:14
for AP being AffinPlane st AP is Moufangian holds
AP is translational
proof
let AP be AffinPlane; ::_thesis: ( AP is Moufangian implies AP is translational )
assume AP is Moufangian ; ::_thesis: AP is translational
then AP is satisfying_des_1 by Th3, Th13;
hence AP is translational by Th7; ::_thesis: verum
end;
theorem :: AFF_2:15
for AP being AffinPlane st AP is translational holds
AP is satisfying_pap
proof
let AP be AffinPlane; ::_thesis: ( AP is translational implies AP is satisfying_pap )
assume A1: AP is translational ; ::_thesis: AP is satisfying_pap
let M be Subset of AP; :: according to AFF_2:def_13 ::_thesis: for N being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let N be Subset of AP; ::_thesis: for a, b, c, a9, b9, c9 being Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
let a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that
A2: M is being_line and
A3: N is being_line and
A4: a in M and
A5: b in M and
A6: c in M and
A7: M // N and
A8: M <> N and
A9: a9 in N and
A10: b9 in N and
A11: c9 in N and
A12: a,b9 // b,a9 and
A13: b,c9 // c,b9 ; ::_thesis: a,c9 // c,a9
set A = Line (a,b9);
set A9 = Line (b,a9);
set P = Line (b,c9);
set P9 = Line (c,b9);
A14: c <> b9 by A6, A7, A8, A10, AFF_1:45;
then A15: ( c in Line (c,b9) & b9 in Line (c,b9) ) by AFF_1:24;
A16: b <> c9 by A5, A7, A8, A11, AFF_1:45;
then A17: ( Line (b,c9) is being_line & b in Line (b,c9) ) by AFF_1:24;
A18: Line (c,b9) is being_line by A14, AFF_1:24;
then consider C9 being Subset of AP such that
A19: a in C9 and
A20: Line (c,b9) // C9 by AFF_1:49;
A21: C9 is being_line by A20, AFF_1:36;
assume A22: not a,c9 // c,a9 ; ::_thesis: contradiction
A23: now__::_thesis:_not_a_=_c
assume A24: a = c ; ::_thesis: contradiction
then b,c9 // b,a9 by A12, A13, A14, AFF_1:5;
then LIN b,c9,a9 by AFF_1:def_1;
then LIN a9,c9,b by AFF_1:6;
then ( a9 = c9 or b in N ) by A3, A9, A11, AFF_1:25;
hence contradiction by A5, A7, A8, A22, A24, AFF_1:2, AFF_1:45; ::_thesis: verum
end;
A25: Line (c,b9) <> C9
proof
assume Line (c,b9) = C9 ; ::_thesis: contradiction
then LIN a,c,b9 by A18, A15, A19, AFF_1:21;
then b9 in M by A2, A4, A6, A23, AFF_1:25;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
A26: c9 in Line (b,c9) by A16, AFF_1:24;
then A27: Line (c,b9) // Line (b,c9) by A13, A16, A14, A18, A17, A15, AFF_1:38;
A28: now__::_thesis:_not_b_=_c
assume A29: b = c ; ::_thesis: contradiction
then LIN b,c9,b9 by A13, AFF_1:def_1;
then LIN b9,c9,b by AFF_1:6;
then ( b9 = c9 or b in N ) by A3, A10, A11, AFF_1:25;
hence contradiction by A5, A7, A8, A12, A22, A29, AFF_1:45; ::_thesis: verum
end;
A30: Line (c,b9) <> Line (b,c9)
proof
assume Line (c,b9) = Line (b,c9) ; ::_thesis: contradiction
then LIN b,c,b9 by A17, A15, AFF_1:21;
then b9 in M by A2, A5, A6, A28, AFF_1:25;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
A31: a <> b9 by A4, A7, A8, A10, AFF_1:45;
then A32: Line (a,b9) is being_line by AFF_1:24;
then consider C being Subset of AP such that
A33: c in C and
A34: Line (a,b9) // C by AFF_1:49;
A35: C is being_line by A34, AFF_1:36;
A36: a,b // b9,a9 by A4, A5, A7, A9, A10, AFF_1:39;
A37: b9,c9 // c,b by A5, A6, A7, A10, A11, AFF_1:39;
A38: b <> a9 by A5, A7, A8, A9, AFF_1:45;
then A39: a9 in Line (b,a9) by AFF_1:24;
A40: ( a in Line (a,b9) & b9 in Line (a,b9) ) by A31, AFF_1:24;
A41: Line (a,b9) <> C
proof
assume Line (a,b9) = C ; ::_thesis: contradiction
then LIN a,c,b9 by A32, A40, A33, AFF_1:21;
then b9 in M by A2, A4, A6, A23, AFF_1:25;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
not C // C9
proof
assume C // C9 ; ::_thesis: contradiction
then Line (a,b9) // C9 by A34, AFF_1:44;
then Line (a,b9) // Line (c,b9) by A20, AFF_1:44;
then b9,a // b9,c by A40, A15, AFF_1:39;
then LIN b9,a,c by AFF_1:def_1;
then LIN a,c,b9 by AFF_1:6;
then b9 in M by A2, A4, A6, A23, AFF_1:25;
hence contradiction by A7, A8, A10, AFF_1:45; ::_thesis: verum
end;
then consider s being Element of AP such that
A42: s in C and
A43: s in C9 by A35, A21, AFF_1:58;
A44: ( Line (b,a9) is being_line & b in Line (b,a9) ) by A38, AFF_1:24;
A45: now__::_thesis:_not_a_=_b
assume A46: a = b ; ::_thesis: contradiction
then LIN a,b9,a9 by A12, AFF_1:def_1;
then LIN a9,b9,a by AFF_1:6;
then ( a9 = b9 or a in N ) by A3, A9, A10, AFF_1:25;
hence contradiction by A4, A7, A8, A13, A22, A46, AFF_1:45; ::_thesis: verum
end;
A47: now__::_thesis:_not_a9_=_b9
assume a9 = b9 ; ::_thesis: contradiction
then a9,a // a9,b by A12, AFF_1:4;
then LIN a9,a,b by AFF_1:def_1;
then LIN a,b,a9 by AFF_1:6;
then a9 in M by A2, A4, A5, A45, AFF_1:25;
hence contradiction by A7, A8, A9, AFF_1:45; ::_thesis: verum
end;
A48: Line (a,b9) <> Line (b,a9)
proof
assume Line (a,b9) = Line (b,a9) ; ::_thesis: contradiction
then LIN a9,b9,a by A32, A40, A39, AFF_1:21;
then a in N by A3, A9, A10, A47, AFF_1:25;
hence contradiction by A4, A7, A8, AFF_1:45; ::_thesis: verum
end;
A49: b <> s
proof
assume b = s ; ::_thesis: contradiction
then a,b9 // b,c by A40, A33, A34, A42, AFF_1:39;
then b,a9 // b,c by A12, A31, AFF_1:5;
then LIN b,a9,c by AFF_1:def_1;
then LIN b,c,a9 by AFF_1:6;
then a9 in M by A2, A5, A6, A28, AFF_1:25;
hence contradiction by A7, A8, A9, AFF_1:45; ::_thesis: verum
end;
A50: Line (a,b9) // Line (b,a9) by A12, A31, A38, AFF_1:37;
a,s // b9,c by A15, A19, A20, A43, AFF_1:39;
then A51: b,s // a9,c by A1, A32, A40, A44, A39, A33, A34, A35, A42, A36, A48, A41, A50, Def11;
b9,a // c,s by A40, A33, A34, A42, AFF_1:39;
then c9,a // b,s by A1, A18, A17, A26, A15, A19, A20, A21, A43, A37, A30, A25, A27, Def11;
then c9,a // a9,c by A51, A49, AFF_1:5;
hence contradiction by A22, AFF_1:4; ::_thesis: verum
end;