:: CONMETR1 semantic presentation

definition

let X be AffinPlane;
attr X is satisfying_minor_Scherungssatz means :Def1: :: 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;

end;

:: deftheorem Def1 defines satisfying_minor_Scherungssatz CONMETR1:def 1 :

notation

let X be AffinPlane;
synonym X satisfies_minor_SCH for satisfying_minor_Scherungssatz X;

end;

definition

let X be AffinPlane;
attr X is satisfying_major_Scherungssatz means :Def2: :: 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;

end;

:: deftheorem Def2 defines satisfying_major_Scherungssatz CONMETR1:def 2 :

notation

let X be AffinPlane;
synonym X satisfies_major_SCH for satisfying_major_Scherungssatz X;

end;

definition

let X be AffinPlane;
attr X is satisfying_Scherungssatz means :Def3: :: 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;

end;

:: deftheorem Def3 defines satisfying_Scherungssatz CONMETR1:def 3 :

notation

let X be AffinPlane;
synonym X satisfies_SCH for satisfying_Scherungssatz X;

end;

definition

let X be AffinPlane;
attr X is satisfying_indirect_Scherungssatz means :Def4: :: 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;

end;

:: deftheorem Def4 defines satisfying_indirect_Scherungssatz CONMETR1:def 4 :

notation

let X be AffinPlane;
synonym X satisfies_SCH* for satisfying_indirect_Scherungssatz X;

end;

definition

let X be AffinPlane;
attr X is satisfying_minor_indirect_Scherungssatz means :Def5: :: 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;

end;

:: deftheorem Def5 defines satisfying_minor_indirect_Scherungssatz CONMETR1:def 5 :

notation

let X be AffinPlane;
synonym X satisfies_minor_SCH* for satisfying_minor_indirect_Scherungssatz X;

end;

definition

let X be AffinPlane;
attr X is satisfying_major_indirect_Scherungssatz means :Def6: :: 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;

end;