:: Metric-Affine Configurations in Metric Affine Planes - Part II :: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski :: :: Received October 31, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let X be OrtAfPl; attrX is satisfying_OPAP means :Def1: :: CONMETR:def 1 for o, a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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; attrX is satisfying_PAP means :: CONMETR:def 2 for o, a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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; attrX is satisfying_MH1 means :Def3: :: CONMETR:def 3 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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; attrX is satisfying_MH2 means :Def4: :: CONMETR:def 4 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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; attrX is satisfying_TDES means :Def5: :: CONMETR:def 5 for o, a, a1, b, b1, c, c1 being Element of X 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; attrX is satisfying_SCH means :: CONMETR:def 6 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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; attrX is satisfying_OSCH means :Def7: :: CONMETR:def 7 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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; attrX is satisfying_des means :Def8: :: CONMETR:def 8 for a, a1, b, b1, c, c1 being Element of X 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; :: deftheorem Def1 defines satisfying_OPAP CONMETR:def_1_:_ for X being OrtAfPl holds ( X is satisfying_OPAP iff for o, a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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 ); :: deftheorem defines satisfying_PAP CONMETR:def_2_:_ for X being OrtAfPl holds ( X is satisfying_PAP iff for o, a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def3 defines satisfying_MH1 CONMETR:def_3_:_ for X being OrtAfPl holds ( X is satisfying_MH1 iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def4 defines satisfying_MH2 CONMETR:def_4_:_ for X being OrtAfPl holds ( X is satisfying_MH2 iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def5 defines satisfying_TDES CONMETR:def_5_:_ for X being OrtAfPl holds ( X is satisfying_TDES iff for o, a, a1, b, b1, c, c1 being Element of X 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 ); :: deftheorem defines satisfying_SCH CONMETR:def_6_:_ for X being OrtAfPl holds ( X is satisfying_SCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def7 defines satisfying_OSCH CONMETR:def_7_:_ for X being OrtAfPl holds ( X is satisfying_OSCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def8 defines satisfying_des CONMETR:def_8_:_ for X being OrtAfPl holds ( X is satisfying_des iff for a, a1, b, b1, c, c1 being Element of X 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 ); theorem Th1: :: CONMETR:1 for X being OrtAfPl ex a, b, c being Element of X st ( LIN a,b,c & a <> b & b <> c & c <> a ) proofend; theorem Th2: :: CONMETR:2 for X being OrtAfPl for a, b being Element of X ex c being Element of X st ( LIN a,b,c & a <> c & b <> c ) proofend; theorem Th3: :: CONMETR:3 for X being OrtAfPl for A being Subset of X for a being Element of X st A is being_line holds ex K being Subset of X st ( a in K & A _|_ K ) proofend; theorem Th4: :: CONMETR:4 for X being OrtAfPl for a, b, c being Element of X for A being Subset of X st A is being_line & a in A & b in A & c in A holds LIN a,b,c proofend; theorem Th5: :: CONMETR:5 for X being OrtAfPl for a, b being Element of X for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds A = M proofend; theorem Th6: :: CONMETR:6 for X being OrtAfPl for a, b, c, d being Element of X for M being Subset of X for M9 being Subset of (Af X) for c9, d9 being Element of (Af X) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds c,d // a,b proofend; theorem Th7: :: CONMETR:7 for X being OrtAfPl st X is satisfying_TDES holds Af X is Moufangian proofend; theorem Th8: :: CONMETR:8 for X being OrtAfPl st Af X is translational holds X is satisfying_des proofend; theorem :: CONMETR:9 for X being OrtAfPl st X is satisfying_MH1 holds X is satisfying_OSCH proofend; theorem :: CONMETR:10 for X being OrtAfPl st X is satisfying_MH2 holds X is satisfying_OSCH proofend; theorem :: CONMETR:11 for X being OrtAfPl st X is satisfying_AH holds X is satisfying_TDES proofend; theorem :: CONMETR:12 for X being OrtAfPl st X is satisfying_OSCH & X is satisfying_TDES holds X is satisfying_SCH proofend; theorem :: CONMETR:13 for X being OrtAfPl st X is satisfying_OPAP & X is satisfying_DES holds X is satisfying_PAP proofend; theorem :: CONMETR:14 for X being OrtAfPl st X is satisfying_MH1 & X is satisfying_MH2 holds X is satisfying_OPAP proofend; theorem :: CONMETR:15 for X being OrtAfPl st X is satisfying_3H holds X is satisfying_OPAP proofend;