:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski

::

:: Received October 31, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let X be OrtAfPl;

end;
attr X is satisfying_OPAP means :: 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;

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;

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 :: 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;

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 :: 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;

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 :: 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;

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;

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 :: 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;

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 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 );

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 );

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 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 );

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 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 );

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 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 );

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 );

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 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 );

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 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 );

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 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 )

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 )

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

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

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 AffinStruct(# the carrier of X, the CONGR of X #)

for c9, d9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds

c,d // a,b

for a, b, c, d being Element of X

for M being Subset of X

for M9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #)

for c9, d9 being Element of AffinStruct(# the carrier of X, the CONGR of 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

AffinStruct(# the carrier of X, the CONGR of X #) is Moufangian

AffinStruct(# the carrier of X, the CONGR of X #) is Moufangian

proof end;

theorem Th8: :: CONMETR:8

for X being OrtAfPl st AffinStruct(# the carrier of X, the CONGR of X #) is translational holds

X is satisfying_des

X is satisfying_des

proof end;