:: Classical Configurations in Affine Planes :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received April 13, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users 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 ) proofend; theorem :: AFF_2:2 for AP being AffinPlane holds ( AP is Desarguesian iff AP is satisfying_DES_1 ) proofend; theorem Th3: :: AFF_2:3 for AP being AffinPlane st AP is Moufangian holds AP is satisfying_TDES_1 proofend; theorem :: AFF_2:4 for AP being AffinPlane st AP is satisfying_TDES_1 holds AP is satisfying_TDES_2 proofend; theorem :: AFF_2:5 for AP being AffinPlane st AP is satisfying_TDES_2 holds AP is satisfying_TDES_3 proofend; theorem :: AFF_2:6 for AP being AffinPlane st AP is satisfying_TDES_3 holds AP is Moufangian proofend; theorem Th7: :: AFF_2:7 for AP being AffinPlane holds ( AP is translational iff AP is satisfying_des_1 ) proofend; theorem :: AFF_2:8 for AP being AffinPlane holds ( AP is satisfying_pap iff AP is satisfying_pap_1 ) proofend; theorem Th9: :: AFF_2:9 for AP being AffinPlane st AP is Pappian holds AP is satisfying_pap proofend; theorem Th10: :: AFF_2:10 for AP being AffinPlane holds ( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) ) proofend; theorem :: AFF_2:11 for AP being AffinPlane st AP is Pappian holds AP is Desarguesian proofend; theorem :: AFF_2:12 for AP being AffinPlane st AP is Desarguesian holds AP is Moufangian proofend; theorem Th13: :: AFF_2:13 for AP being AffinPlane st AP is satisfying_TDES_1 holds AP is satisfying_des_1 proofend; theorem :: AFF_2:14 for AP being AffinPlane st AP is Moufangian holds AP is translational proofend; theorem :: AFF_2:15 for AP being AffinPlane st AP is translational holds AP is satisfying_pap proofend;