:: 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;