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

::

:: Received April 19, 1991

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

definition

let X be AffinPlane;

end;
attr X is satisfying_minor_Scherungssatz means :: CONMETR1:def 1

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_minor_Scherungssatz CONMETR1:def 1 :

for X being AffinPlane holds

( X is satisfying_minor_Scherungssatz 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 AffinPlane holds

( X is satisfying_minor_Scherungssatz 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 );

definition

let X be AffinPlane;

end;
attr X is satisfying_major_Scherungssatz means :: CONMETR1:def 2

for o, 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 & o in M & o in 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 o, 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 & o in M & o in 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_major_Scherungssatz CONMETR1:def 2 :

for X being AffinPlane holds

( X is satisfying_major_Scherungssatz iff for o, 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 & o in M & o in 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 AffinPlane holds

( X is satisfying_major_Scherungssatz iff for o, 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 & o in M & o in 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 );

definition

let X be AffinPlane;

end;
attr X is satisfying_Scherungssatz means :: CONMETR1:def 3

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;

:: deftheorem defines satisfying_Scherungssatz CONMETR1:def 3 :

for X being AffinPlane holds

( X is satisfying_Scherungssatz 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 AffinPlane holds

( X is satisfying_Scherungssatz 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 );

definition

let X be AffinPlane;

end;
attr X is satisfying_indirect_Scherungssatz means :: CONMETR1:def 4

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 & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 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 & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4;

:: deftheorem defines satisfying_indirect_Scherungssatz CONMETR1:def 4 :

for X being AffinPlane holds

( X is satisfying_indirect_Scherungssatz 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 & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4 );

for X being AffinPlane holds

( X is satisfying_indirect_Scherungssatz 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 & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4 );

definition

let X be AffinPlane;

end;
attr X is satisfying_minor_indirect_Scherungssatz means :: CONMETR1:def 5

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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 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 & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4;

:: deftheorem defines satisfying_minor_indirect_Scherungssatz CONMETR1:def 5 :

for X being AffinPlane holds

( X is satisfying_minor_indirect_Scherungssatz 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4 );

for X being AffinPlane holds

( X is satisfying_minor_indirect_Scherungssatz 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4 );

definition

let X be AffinPlane;

end;
attr X is satisfying_major_indirect_Scherungssatz means :: CONMETR1:def 6

for o, 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 & o in M & o in 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4;

for o, 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 & o in M & o in 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4;

:: deftheorem defines satisfying_major_indirect_Scherungssatz CONMETR1:def 6 :

for X being AffinPlane holds

( X is satisfying_major_indirect_Scherungssatz iff for o, 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 & o in M & o in 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4 );

for X being AffinPlane holds

( X is satisfying_major_indirect_Scherungssatz iff for o, 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 & o in M & o in 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4 );

theorem Th1: :: CONMETR1:1

for X being AffinPlane holds

( X is satisfying_indirect_Scherungssatz iff ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) )

( X is satisfying_indirect_Scherungssatz iff ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) )

proof end;

theorem Th2: :: CONMETR1:2

for X being AffinPlane holds

( X is satisfying_Scherungssatz iff ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) )

( X is satisfying_Scherungssatz iff ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) )

proof end;

theorem Th3: :: CONMETR1:3

for X being AffinPlane st X is satisfying_minor_indirect_Scherungssatz holds

X is satisfying_minor_Scherungssatz

X is satisfying_minor_Scherungssatz

proof end;

theorem Th4: :: CONMETR1:4

for X being AffinPlane st X is satisfying_major_indirect_Scherungssatz holds

X is satisfying_major_Scherungssatz

X is satisfying_major_Scherungssatz

proof end;

theorem :: CONMETR1:5

for X being AffinPlane st X is satisfying_indirect_Scherungssatz holds

X is satisfying_Scherungssatz

X is satisfying_Scherungssatz

proof end;

theorem Th9: :: CONMETR1:9

for X being AffinPlane holds

( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz )

( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz )

proof end;

theorem :: CONMETR1:12

for X being AffinPlane st X is satisfying_major_indirect_Scherungssatz holds

X is satisfying_minor_indirect_Scherungssatz

X is satisfying_minor_indirect_Scherungssatz

proof end;

theorem :: CONMETR1:13

for X being OrtAfPl holds

( AffinStruct(# the U1 of X, the CONGR of X #) is satisfying_Scherungssatz iff X is satisfying_SCH )

( AffinStruct(# the U1 of X, the CONGR of X #) is satisfying_Scherungssatz iff X is satisfying_SCH )

proof end;

theorem :: CONMETR1:14

for X being OrtAfPl holds

( X is satisfying_TDES iff AffinStruct(# the U1 of X, the CONGR of X #) is Moufangian )

( X is satisfying_TDES iff AffinStruct(# the U1 of X, the CONGR of X #) is Moufangian )

proof end;

theorem :: CONMETR1:15

for X being OrtAfPl holds

( AffinStruct(# the U1 of X, the CONGR of X #) is translational iff X is satisfying_des )

( AffinStruct(# the U1 of X, the CONGR of X #) is translational iff X is satisfying_des )

proof end;

theorem :: CONMETR1:16

for X being OrtAfPl holds

( X is satisfying_PAP iff AffinStruct(# the U1 of X, the CONGR of X #) is Pappian )

( X is satisfying_PAP iff AffinStruct(# the U1 of X, the CONGR of X #) is Pappian )

proof end;

theorem :: CONMETR1:17

for X being OrtAfPl holds

( X is satisfying_DES iff AffinStruct(# the U1 of X, the CONGR of X #) is Desarguesian )

( X is satisfying_DES iff AffinStruct(# the U1 of X, the CONGR of X #) is Desarguesian )

proof end;