:: Metric-Affine Configurations in Metric Affine Planes - Part II :: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski :: :: Received October 31, 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 ANALMETR, SUBSET_1, SYMSP_1, ANALOAF, AFF_1, DIRAF, INCSP_1, AFF_2, CONAFFM, STRUCT_0, CONMETR; notations SUBSET_1, STRUCT_0, ANALOAF, AFF_1, ANALMETR, AFF_2, CONAFFM; constructors AFF_1, AFF_2, CONAFFM; registrations ANALMETR; requirements SUBSET; begin reserve X for OrtAfPl; reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,c3,d,d1,d2,d3,d4,e1,e2 for Element of X; reserve a29,a39,b29,x9 for Element of the AffinStruct of X; reserve A,K,M,N for Subset of X; reserve A9,K9 for Subset of the AffinStruct of X; definition let X; attr X is satisfying_OPAP means :: CONMETR:def 1 for o,a1,a2,a3,b1,b2,b3,M,N st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds a1,b2 // a2,b3; attr X is satisfying_PAP means :: CONMETR:def 2 for o,a1,a2,a3,b1,b2,b3,M,N st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds a1,b2 // a2,b3; attr X is satisfying_MH1 means :: CONMETR:def 3 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds a1,a4 _|_ b1,b4; attr X is satisfying_MH2 means :: CONMETR:def 4 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M _|_ N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds a1,a4 _|_ b1,b4; attr X is satisfying_TDES means :: CONMETR:def 5 for o,a,a1,b,b1,c,c1 st o<>a & o<>a1 & o<>b & o<>b1 & o<>c & o<>c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds a,c // a1,c1; attr X is satisfying_SCH means :: CONMETR:def 6 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3, b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4; attr X is satisfying_OSCH means :: CONMETR:def 7 for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1, a4 // b1,b4 holds a3,a4 // b3,b4; attr X is satisfying_des means :: CONMETR:def 8 for a,a1,b,b1,c,c1 st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds b,c // b1,c1; end; theorem :: CONMETR:1 ex a,b,c st LIN a,b,c & a<>b & b<>c & c <>a; theorem :: CONMETR:2 for a,b ex c st LIN a,b,c & a<>c & b<>c; theorem :: CONMETR:3 for A,a st A is being_line ex K st a in K & A _|_ K; theorem :: CONMETR:4 A is being_line & a in A & b in A & c in A implies LIN a,b,c; theorem :: CONMETR:5 A is being_line & M is being_line & a in A & b in A & a in M & b in M implies a=b or A=M; theorem :: CONMETR:6 for a,b,c,d,M holds for M9 being Subset of the AffinStruct of X, c9,d9 being Element of the AffinStruct of X st c =c9 & d=d9 & M=M9 & a in M & b in M & c9,d9 // M9 holds c,d // a,b; theorem :: CONMETR:7 X is satisfying_TDES implies the AffinStruct of X is Moufangian; theorem :: CONMETR:8 the AffinStruct of X is translational implies X is satisfying_des; theorem :: CONMETR:9 X is satisfying_MH1 implies X is satisfying_OSCH; theorem :: CONMETR:10 X is satisfying_MH2 implies X is satisfying_OSCH; theorem :: CONMETR:11 X is satisfying_AH implies X is satisfying_TDES; theorem :: CONMETR:12 X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH; theorem :: CONMETR:13 X is satisfying_OPAP & X is satisfying_DES implies X is satisfying_PAP; theorem :: CONMETR:14 X is satisfying_MH1 & X is satisfying_MH2 implies X is satisfying_OPAP; theorem :: CONMETR:15 X is satisfying_3H implies X is satisfying_OPAP;