:: Affine Localizations of Desargues Axiom :: by Eugeniusz Kusak, Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received April 26, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies DIRAF, SUBSET_1, AFF_1, ANALOAF, INCSP_1, AFF_2, AFF_3; notations STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2; constructors AFF_1, AFF_2; registrations STRUCT_0; begin reserve AP for AffinPlane; reserve a,a9,b,b9,c,c9,d,x,y,o,p,q for Element of AP; reserve A,C,D9,M,N,P for Subset of AP; definition let AP; attr AP is satisfying_DES1 means :: AFF_3:def 1 for A,P,C,o,a,a9,b,b9,c,c9,p,q 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; definition let AP; attr AP is satisfying_DES1_1 means :: AFF_3:def 2 for A,P,C,o,a,a9,b,b9,c,c9,p,q 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; definition let AP; attr AP is satisfying_DES1_2 means :: AFF_3:def 3 for A,P,C,o,a,a9,b,b9,c,c9,p,q 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; definition let AP; attr AP is satisfying_DES1_3 means :: AFF_3:def 4 for A,P,C,o,a,a9,b,b9,c,c9,p,q 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; definition let AP; attr AP is satisfying_DES2 means :: AFF_3:def 5 for A,P,C,a,a9,b,b9,c,c9,p,q 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; definition let AP; attr AP is satisfying_DES2_1 means :: AFF_3:def 6 for A,P,C,a,a9,b,b9,c,c9,p,q 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; definition let AP; attr AP is satisfying_DES2_2 means :: AFF_3:def 7 for A,P,C,a,a9,b,b9,c,c9,p,q 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; definition let AP; attr AP is satisfying_DES2_3 means :: AFF_3:def 8 for A,P,C,a,a9,b,b9,c,c9,p,q 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; theorem :: AFF_3:1 AP is satisfying_DES1 implies AP is satisfying_DES1_1; theorem :: AFF_3:2 AP is satisfying_DES1_1 implies AP is satisfying_DES1; theorem :: AFF_3:3 AP is Desarguesian implies AP is satisfying_DES1; theorem :: AFF_3:4 AP is Desarguesian implies AP is satisfying_DES1_2; theorem :: AFF_3:5 AP is satisfying_DES1_2 implies AP is satisfying_DES1_3; theorem :: AFF_3:6 AP is satisfying_DES1_2 implies AP is Desarguesian; theorem :: AFF_3:7 AP is satisfying_DES2_1 implies AP is satisfying_DES2; theorem :: AFF_3:8 AP is satisfying_DES2_1 iff AP is satisfying_DES2_3; theorem :: AFF_3:9 AP is satisfying_DES2 iff AP is satisfying_DES2_2; theorem :: AFF_3:10 AP is satisfying_DES1_3 implies AP is satisfying_DES2_1;