:: Metric-Affine Configurations in Metric Affine Planes - Part II
:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received October 31, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

let X be OrtAfPl;
attr X 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;
attr X 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;
attr X 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;
attr X 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;
attr X 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;
attr X 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;
attr X 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;
attr X 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 )

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th7: :: CONMETR:7

for X being OrtAfPl st X is satisfying_TDES holds
Af X is Moufangian

proof end;

theorem Th8: :: CONMETR:8

for X being OrtAfPl st Af X is translational holds
X is satisfying_des

proof end;

theorem :: CONMETR:9

for X being OrtAfPl st X is satisfying_MH1 holds
X is satisfying_OSCH

proof end;

theorem :: CONMETR:10

for X being OrtAfPl st X is satisfying_MH2 holds
X is satisfying_OSCH

proof end;

theorem :: CONMETR:11

for X being OrtAfPl st X is satisfying_AH holds
X is satisfying_TDES

proof end;

theorem :: CONMETR:12

for X being OrtAfPl st X is satisfying_OSCH & X is satisfying_TDES holds
X is satisfying_SCH

proof end;

theorem :: CONMETR:13

for X being OrtAfPl st X is satisfying_OPAP & X is satisfying_DES holds
X is satisfying_PAP

proof end;

theorem :: CONMETR:14

for X being OrtAfPl st X is satisfying_MH1 & X is satisfying_MH2 holds
X is satisfying_OPAP

proof end;

theorem :: CONMETR:15

for X being OrtAfPl st X is satisfying_3H holds
X is satisfying_OPAP

proof end;