:: CONMETR1 semantic presentation

definition
let c1 be AffinPlane;
attr a1 is satisfying_minor_Scherungssatz means :Def1: :: CONMETR1:def 1
for b1, b2, b3, b4, b5, b6, b7, b8 being Element of a1
for b9, b10 being Subset of a1 st b9 // b10 & b1 in b9 & b3 in b9 & b5 in b9 & b7 in b9 & b2 in b10 & b4 in b10 & b6 in b10 & b8 in b10 & not b4 in b9 & not b2 in b9 & not b6 in b9 & not b8 in b9 & not b1 in b10 & not b3 in b10 & not b5 in b10 & not b7 in b10 & b3,b2 // b7,b6 & b2,b1 // b6,b5 & b1,b4 // b5,b8 holds
b3,b4 // b7,b8;
end;

:: deftheorem Def1 defines satisfying_minor_Scherungssatz CONMETR1:def 1 :
for b1 being AffinPlane holds
( b1 is satisfying_minor_Scherungssatz iff for b2, b3, b4, b5, b6, b7, b8, b9 being Element of b1
for b10, b11 being Subset of b1 st b10 // b11 & b2 in b10 & b4 in b10 & b6 in b10 & b8 in b10 & b3 in b11 & b5 in b11 & b7 in b11 & b9 in b11 & not b5 in b10 & not b3 in b10 & not b7 in b10 & not b9 in b10 & not b2 in b11 & not b4 in b11 & not b6 in b11 & not b8 in b11 & b4,b3 // b8,b7 & b3,b2 // b7,b6 & b2,b5 // b6,b9 holds
b4,b5 // b8,b9 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_minor_SCH for satisfying_minor_Scherungssatz c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_major_Scherungssatz means :Def2: :: CONMETR1:def 2
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being Element of a1
for b10, b11 being Subset of a1 st b10 is being_line & b11 is being_line & b1 in b10 & b1 in b11 & b2 in b10 & b4 in b10 & b6 in b10 & b8 in b10 & b3 in b11 & b5 in b11 & b7 in b11 & b9 in b11 & not b5 in b10 & not b3 in b10 & not b7 in b10 & not b9 in b10 & not b2 in b11 & not b4 in b11 & not b6 in b11 & not b8 in b11 & b4,b3 // b8,b7 & b3,b2 // b7,b6 & b2,b5 // b6,b9 holds
b4,b5 // b8,b9;
end;

:: deftheorem Def2 defines satisfying_major_Scherungssatz CONMETR1:def 2 :
for b1 being AffinPlane holds
( b1 is satisfying_major_Scherungssatz iff for b2, b3, b4, b5, b6, b7, b8, b9, b10 being Element of b1
for b11, b12 being Subset of b1 st b11 is being_line & b12 is being_line & b2 in b11 & b2 in b12 & b3 in b11 & b5 in b11 & b7 in b11 & b9 in b11 & b4 in b12 & b6 in b12 & b8 in b12 & b10 in b12 & not b6 in b11 & not b4 in b11 & not b8 in b11 & not b10 in b11 & not b3 in b12 & not b5 in b12 & not b7 in b12 & not b9 in b12 & b5,b4 // b9,b8 & b4,b3 // b8,b7 & b3,b6 // b7,b10 holds
b5,b6 // b9,b10 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_major_SCH for satisfying_major_Scherungssatz c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_Scherungssatz means :Def3: :: CONMETR1:def 3
for b1, b2, b3, b4, b5, b6, b7, b8 being Element of a1
for b9, b10 being Subset of a1 st b9 is being_line & b10 is being_line & b1 in b9 & b3 in b9 & b5 in b9 & b7 in b9 & b2 in b10 & b4 in b10 & b6 in b10 & b8 in b10 & not b4 in b9 & not b2 in b9 & not b6 in b9 & not b8 in b9 & not b1 in b10 & not b3 in b10 & not b5 in b10 & not b7 in b10 & b3,b2 // b7,b6 & b2,b1 // b6,b5 & b1,b4 // b5,b8 holds
b3,b4 // b7,b8;
end;

:: deftheorem Def3 defines satisfying_Scherungssatz CONMETR1:def 3 :
for b1 being AffinPlane holds
( b1 is satisfying_Scherungssatz iff for b2, b3, b4, b5, b6, b7, b8, b9 being Element of b1
for b10, b11 being Subset of b1 st b10 is being_line & b11 is being_line & b2 in b10 & b4 in b10 & b6 in b10 & b8 in b10 & b3 in b11 & b5 in b11 & b7 in b11 & b9 in b11 & not b5 in b10 & not b3 in b10 & not b7 in b10 & not b9 in b10 & not b2 in b11 & not b4 in b11 & not b6 in b11 & not b8 in b11 & b4,b3 // b8,b7 & b3,b2 // b7,b6 & b2,b5 // b6,b9 holds
b4,b5 // b8,b9 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_SCH for satisfying_Scherungssatz c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_indirect_Scherungssatz means :Def4: :: CONMETR1:def 4
for b1, b2, b3, b4, b5, b6, b7, b8 being Element of a1
for b9, b10 being Subset of a1 st b9 is being_line & b10 is being_line & b1 in b9 & b3 in b9 & b6 in b9 & b8 in b9 & b2 in b10 & b4 in b10 & b5 in b10 & b7 in b10 & not b4 in b9 & not b2 in b9 & not b5 in b9 & not b7 in b9 & not b1 in b10 & not b3 in b10 & not b6 in b10 & not b8 in b10 & b3,b2 // b7,b6 & b2,b1 // b6,b5 & b1,b4 // b5,b8 holds
b3,b4 // b7,b8;
end;

:: deftheorem Def4 defines satisfying_indirect_Scherungssatz CONMETR1:def 4 :
for b1 being AffinPlane holds
( b1 is satisfying_indirect_Scherungssatz iff for b2, b3, b4, b5, b6, b7, b8, b9 being Element of b1
for b10, b11 being Subset of b1 st b10 is being_line & b11 is being_line & b2 in b10 & b4 in b10 & b7 in b10 & b9 in b10 & b3 in b11 & b5 in b11 & b6 in b11 & b8 in b11 & not b5 in b10 & not b3 in b10 & not b6 in b10 & not b8 in b10 & not b2 in b11 & not b4 in b11 & not b7 in b11 & not b9 in b11 & b4,b3 // b8,b7 & b3,b2 // b7,b6 & b2,b5 // b6,b9 holds
b4,b5 // b8,b9 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_SCH* for satisfying_indirect_Scherungssatz c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_minor_indirect_Scherungssatz means :Def5: :: CONMETR1:def 5
for b1, b2, b3, b4, b5, b6, b7, b8 being Element of a1
for b9, b10 being Subset of a1 st b9 // b10 & b1 in b9 & b3 in b9 & b6 in b9 & b8 in b9 & b2 in b10 & b4 in b10 & b5 in b10 & b7 in b10 & not b4 in b9 & not b2 in b9 & not b5 in b9 & not b7 in b9 & not b1 in b10 & not b3 in b10 & not b6 in b10 & not b8 in b10 & b3,b2 // b7,b6 & b2,b1 // b6,b5 & b1,b4 // b5,b8 holds
b3,b4 // b7,b8;
end;

:: deftheorem Def5 defines satisfying_minor_indirect_Scherungssatz CONMETR1:def 5 :
for b1 being AffinPlane holds
( b1 is satisfying_minor_indirect_Scherungssatz iff for b2, b3, b4, b5, b6, b7, b8, b9 being Element of b1
for b10, b11 being Subset of b1 st b10 // b11 & b2 in b10 & b4 in b10 & b7 in b10 & b9 in b10 & b3 in b11 & b5 in b11 & b6 in b11 & b8 in b11 & not b5 in b10 & not b3 in b10 & not b6 in b10 & not b8 in b10 & not b2 in b11 & not b4 in b11 & not b7 in b11 & not b9 in b11 & b4,b3 // b8,b7 & b3,b2 // b7,b6 & b2,b5 // b6,b9 holds
b4,b5 // b8,b9 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_minor_SCH* for satisfying_minor_indirect_Scherungssatz c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_major_indirect_Scherungssatz means :Def6: :: CONMETR1:def 6
for b1, b2, b3, b4, b5, b6, b7, b8, b9 being Element of a1
for b10, b11 being Subset of a1 st b10 is being_line & b11 is being_line & b1 in b10 & b1 in b11 & b2 in b10 & b4 in b10 & b7 in b10 & b9 in b10 & b3 in b11 & b5 in b11 & b6 in b11 & b8 in b11 & not b5 in b10 & not b3 in b10 & not b6 in b10 & not b8 in b10 & not b2 in b11 & not b4 in b11 & not b7 in b11 & not b9 in b11 & b4,b3 // b8,b7 & b3,b2 // b7,b6 & b2,b5 // b6,b9 holds
b4,b5 // b8,b9;
end;

:: deftheorem Def6 defines satisfying_major_indirect_Scherungssatz CONMETR1:def 6 :
for b1 being AffinPlane holds
( b1 is satisfying_major_indirect_Scherungssatz iff for b2, b3, b4, b5, b6, b7, b8, b9, b10 being Element of b1
for b11, b12 being Subset of b1 st b11 is being_line & b12 is being_line & b2 in b11 & b2 in b12 & b3 in b11 & b5 in b11 & b8 in b11 & b10 in b11 & b4 in b12 & b6 in b12 & b7 in b12 & b9 in b12 & not b6 in b11 & not b4 in b11 & not b7 in b11 & not b9 in b11 & not b3 in b12 & not b5 in b12 & not b8 in b12 & not b10 in b12 & b5,b4 // b9,b8 & b4,b3 // b8,b7 & b3,b6 // b7,b10 holds
b5,b6 // b9,b10 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_major_SCH* for satisfying_major_indirect_Scherungssatz c1;
end;

theorem Th1: :: CONMETR1:1
for b1 being AffinPlane holds
( b1 satisfies_SCH* iff ( b1 satisfies_minor_SCH* & b1 satisfies_major_SCH* ) )
proof end;

theorem Th2: :: CONMETR1:2
for b1 being AffinPlane holds
( b1 satisfies_SCH iff ( b1 satisfies_minor_SCH & b1 satisfies_major_SCH ) )
proof end;

theorem Th3: :: CONMETR1:3
for b1 being AffinPlane st b1 satisfies_minor_SCH* holds
b1 satisfies_minor_SCH
proof end;

theorem Th4: :: CONMETR1:4
for b1 being AffinPlane st b1 satisfies_major_SCH* holds
b1 satisfies_major_SCH
proof end;

theorem Th5: :: CONMETR1:5
for b1 being AffinPlane st b1 satisfies_SCH* holds
b1 satisfies_SCH
proof end;

theorem Th6: :: CONMETR1:6
for b1 being AffinPlane st b1 satisfies_des holds
b1 satisfies_minor_SCH
proof end;

theorem Th7: :: CONMETR1:7
for b1 being AffinPlane st b1 satisfies_DES holds
b1 satisfies_major_SCH
proof end;

theorem Th8: :: CONMETR1:8
for b1 being AffinPlane holds
( b1 satisfies_DES iff b1 satisfies_SCH )
proof end;

theorem Th9: :: CONMETR1:9
for b1 being AffinPlane holds
( b1 satisfies_pap iff b1 satisfies_minor_SCH* )
proof end;

theorem Th10: :: CONMETR1:10
for b1 being AffinPlane holds
( b1 satisfies_PAP iff b1 satisfies_major_SCH* )
proof end;

theorem Th11: :: CONMETR1:11
for b1 being AffinPlane holds
( b1 satisfies_PPAP iff b1 satisfies_SCH* )
proof end;

theorem Th12: :: CONMETR1:12
for b1 being AffinPlane st b1 satisfies_major_SCH* holds
b1 satisfies_minor_SCH*
proof end;

theorem Th13: :: CONMETR1:13
for b1 being OrtAfPl holds
( Af b1 satisfies_SCH iff SCH_holds_in b1 )
proof end;

theorem Th14: :: CONMETR1:14
for b1 being OrtAfPl holds
( TDES_holds_in b1 iff Af b1 satisfies_TDES )
proof end;

theorem Th15: :: CONMETR1:15
for b1 being OrtAfPl holds
( Af b1 satisfies_des iff des_holds_in b1 )
proof end;

theorem Th16: :: CONMETR1:16
for b1 being OrtAfPl holds
( PAP_holds_in b1 iff Af b1 satisfies_PAP )
proof end;

theorem Th17: :: CONMETR1:17
for b1 being OrtAfPl holds
( DES_holds_in b1 iff Af b1 satisfies_DES )
proof end;