:: Affine Localizations of Desargues Axiom :: by Eugeniusz Kusak, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received April 26, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let AP be AffinPlane; attrAP is satisfying_DES1 means :Def1: :: AFF_3:def 1 for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q; end; :: deftheorem Def1 defines satisfying_DES1 AFF_3:def_1_:_ for AP being AffinPlane holds ( AP is satisfying_DES1 iff for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q ); definition let AP be AffinPlane; attrAP is satisfying_DES1_1 means :Def2: :: AFF_3:def 2 for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9; end; :: deftheorem Def2 defines satisfying_DES1_1 AFF_3:def_2_:_ for AP being AffinPlane holds ( AP is satisfying_DES1_1 iff for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 ); definition let AP be AffinPlane; attrAP is satisfying_DES1_2 means :Def3: :: AFF_3:def 3 for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in C; end; :: deftheorem Def3 defines satisfying_DES1_2 AFF_3:def_3_:_ for AP being AffinPlane holds ( AP is satisfying_DES1_2 iff for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in C ); definition let AP be AffinPlane; attrAP is satisfying_DES1_3 means :Def4: :: AFF_3:def 4 for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in P; end; :: deftheorem Def4 defines satisfying_DES1_3 AFF_3:def_4_:_ for AP being AffinPlane holds ( AP is satisfying_DES1_3 iff for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in P ); definition let AP be AffinPlane; attrAP is satisfying_DES2 means :Def5: :: AFF_3:def 5 for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q; end; :: deftheorem Def5 defines satisfying_DES2 AFF_3:def_5_:_ for AP being AffinPlane holds ( AP is satisfying_DES2 iff for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q ); definition let AP be AffinPlane; attrAP is satisfying_DES2_1 means :Def6: :: AFF_3:def 6 for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9; end; :: deftheorem Def6 defines satisfying_DES2_1 AFF_3:def_6_:_ for AP being AffinPlane holds ( AP is satisfying_DES2_1 iff for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 ); definition let AP be AffinPlane; attrAP is satisfying_DES2_2 means :Def7: :: AFF_3:def 7 for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // P; end; :: deftheorem Def7 defines satisfying_DES2_2 AFF_3:def_7_:_ for AP being AffinPlane holds ( AP is satisfying_DES2_2 iff for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // P ); definition let AP be AffinPlane; attrAP is satisfying_DES2_3 means :Def8: :: AFF_3:def 8 for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // C; end; :: deftheorem Def8 defines satisfying_DES2_3 AFF_3:def_8_:_ for AP being AffinPlane holds ( AP is satisfying_DES2_3 iff for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // C ); theorem :: AFF_3:1 for AP being AffinPlane st AP is satisfying_DES1 holds AP is satisfying_DES1_1 proofend; theorem :: AFF_3:2 for AP being AffinPlane st AP is satisfying_DES1_1 holds AP is satisfying_DES1 proofend; theorem :: AFF_3:3 for AP being AffinPlane st AP is Desarguesian holds AP is satisfying_DES1 proofend; theorem :: AFF_3:4 for AP being AffinPlane st AP is Desarguesian holds AP is satisfying_DES1_2 proofend; theorem :: AFF_3:5 for AP being AffinPlane st AP is satisfying_DES1_2 holds AP is satisfying_DES1_3 proofend; theorem :: AFF_3:6 for AP being AffinPlane st AP is satisfying_DES1_2 holds AP is Desarguesian proofend; theorem :: AFF_3:7 for AP being AffinPlane st AP is satisfying_DES2_1 holds AP is satisfying_DES2 proofend; theorem :: AFF_3:8 for AP being AffinPlane holds ( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 ) proofend; theorem :: AFF_3:9 for AP being AffinPlane holds ( AP is satisfying_DES2 iff AP is satisfying_DES2_2 ) proofend; theorem :: AFF_3:10 for AP being AffinPlane st AP is satisfying_DES1_3 holds AP is satisfying_DES2_1 proofend;