:: CONMETR semantic presentation

definition
let c1 be OrtAfPl;
attr a1 is satisfying_OPAP means :Def1: :: CONMETR:def 1
for b1, b2, b3, b4, b5, b6, b7 being Element of a1
for b8, b9 being Subset of a1 st b1 in b8 & b2 in b8 & b3 in b8 & b4 in b8 & b1 in b9 & b5 in b9 & b6 in b9 & b7 in b9 & not b6 in b8 & not b4 in b9 & b8 _|_ b9 & b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & b4,b6 // b3,b5 & b4,b7 // b2,b5 holds
b2,b6 // b3,b7;
attr a1 is satisfying_PAP means :: CONMETR:def 2
for b1, b2, b3, b4, b5, b6, b7 being Element of a1
for b8, b9 being Subset of a1 st b8 is_line & b9 is_line & b1 in b8 & b2 in b8 & b3 in b8 & b4 in b8 & b1 in b9 & b5 in b9 & b6 in b9 & b7 in b9 & not b6 in b8 & not b4 in b9 & b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & b4,b6 // b3,b5 & b4,b7 // b2,b5 holds
b2,b6 // b3,b7;
attr a1 is satisfying_MH1 means :Def3: :: CONMETR:def 3
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 b2 in b9 & not b4 in b9 & b1,b2 _|_ b5,b6 & b2,b3 _|_ b6,b7 & b3,b4 _|_ b7,b8 holds
b1,b4 _|_ b5,b8;
attr a1 is satisfying_MH2 means :Def4: :: CONMETR:def 4
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 b2 in b9 & not b4 in b9 & b1,b2 _|_ b5,b6 & b2,b3 _|_ b6,b7 & b3,b4 _|_ b7,b8 holds
b1,b4 _|_ b5,b8;
attr a1 is satisfying_TDES means :Def5: :: CONMETR:def 5
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & not LIN b4,b5,b2 & not LIN b4,b5,b6 & LIN b1,b2,b3 & LIN b1,b4,b5 & LIN b1,b6,b7 & b2,b4 // b3,b5 & b2,b4 // b1,b6 & b4,b6 // b5,b7 holds
b2,b6 // b3,b7;
attr a1 is satisfying_SCH means :: CONMETR:def 6
for b1, b2, b3, b4, b5, b6, b7, b8 being Element of a1
for b9, b10 being Subset of a1 st b9 is_line & b10 is_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;
attr a1 is satisfying_OSCH means :Def7: :: CONMETR:def 7
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;
attr a1 is satisfying_des means :Def8: :: CONMETR:def 8
for b1, b2, b3, b4, b5, b6 being Element of a1 st not LIN b1,b2,b3 & not LIN b1,b2,b5 & b1,b2 // b3,b4 & b1,b2 // b5,b6 & b1,b3 // b2,b4 & b1,b5 // b2,b6 holds
b3,b5 // b4,b6;
end;

:: deftheorem Def1 defines satisfying_OPAP CONMETR:def 1 :
for b1 being OrtAfPl holds
( b1 is satisfying_OPAP iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1
for b9, b10 being Subset of b1 st b2 in b9 & b3 in b9 & b4 in b9 & b5 in b9 & b2 in b10 & b6 in b10 & b7 in b10 & b8 in b10 & not b7 in b9 & not b5 in b10 & b9 _|_ b10 & b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> b8 & b5,b7 // b4,b6 & b5,b8 // b3,b6 holds
b3,b7 // b4,b8 );

:: deftheorem Def2 defines satisfying_PAP CONMETR:def 2 :
for b1 being OrtAfPl holds
( b1 is satisfying_PAP iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1
for b9, b10 being Subset of b1 st b9 is_line & b10 is_line & b2 in b9 & b3 in b9 & b4 in b9 & b5 in b9 & b2 in b10 & b6 in b10 & b7 in b10 & b8 in b10 & not b7 in b9 & not b5 in b10 & b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> b8 & b5,b7 // b4,b6 & b5,b8 // b3,b6 holds
b3,b7 // b4,b8 );

:: deftheorem Def3 defines satisfying_MH1 CONMETR:def 3 :
for b1 being OrtAfPl holds
( b1 is satisfying_MH1 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 b3 in b10 & not b5 in b10 & b2,b3 _|_ b6,b7 & b3,b4 _|_ b7,b8 & b4,b5 _|_ b8,b9 holds
b2,b5 _|_ b6,b9 );

:: deftheorem Def4 defines satisfying_MH2 CONMETR:def 4 :
for b1 being OrtAfPl holds
( b1 is satisfying_MH2 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 b3 in b10 & not b5 in b10 & b2,b3 _|_ b6,b7 & b3,b4 _|_ b7,b8 & b4,b5 _|_ b8,b9 holds
b2,b5 _|_ b6,b9 );

:: deftheorem Def5 defines satisfying_TDES CONMETR:def 5 :
for b1 being OrtAfPl holds
( b1 is satisfying_TDES iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> b8 & not LIN b5,b6,b3 & not LIN b5,b6,b7 & LIN b2,b3,b4 & LIN b2,b5,b6 & LIN b2,b7,b8 & b3,b5 // b4,b6 & b3,b5 // b2,b7 & b5,b7 // b6,b8 holds
b3,b7 // b4,b8 );

:: deftheorem Def6 defines satisfying_SCH CONMETR:def 6 :
for b1 being OrtAfPl holds
( b1 is satisfying_SCH iff for b2, b3, b4, b5, b6, b7, b8, b9 being Element of b1
for b10, b11 being Subset of b1 st b10 is_line & b11 is_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 );

:: deftheorem Def7 defines satisfying_OSCH CONMETR:def 7 :
for b1 being OrtAfPl holds
( b1 is satisfying_OSCH 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 );

:: deftheorem Def8 defines satisfying_des CONMETR:def 8 :
for b1 being OrtAfPl holds
( b1 is satisfying_des iff for b2, b3, b4, b5, b6, b7 being Element of b1 st not LIN b2,b3,b4 & not LIN b2,b3,b6 & b2,b3 // b4,b5 & b2,b3 // b6,b7 & b2,b4 // b3,b5 & b2,b6 // b3,b7 holds
b4,b6 // b5,b7 );

notation
let c1 be OrtAfPl;
synonym OPAP_holds_in c1 for satisfying_OPAP c1;
synonym PAP_holds_in c1 for satisfying_PAP c1;
synonym MH1_holds_in c1 for satisfying_MH1 c1;
synonym MH2_holds_in c1 for satisfying_MH2 c1;
synonym TDES_holds_in c1 for satisfying_TDES c1;
synonym SCH_holds_in c1 for satisfying_SCH c1;
synonym OSCH_holds_in c1 for satisfying_OSCH c1;
synonym des_holds_in c1 for satisfying_des c1;
end;

theorem Th1: :: CONMETR:1
for b1 being OrtAfPl ex b2, b3, b4 being Element of b1 st
( LIN b2,b3,b4 & b2 <> b3 & b3 <> b4 & b4 <> b2 )
proof end;

theorem Th2: :: CONMETR:2
for b1 being OrtAfPl
for b2, b3 being Element of b1 st b2 <> b3 holds
ex b4 being Element of b1 st
( LIN b2,b3,b4 & b2 <> b4 & b3 <> b4 )
proof end;

theorem Th3: :: CONMETR:3
for b1 being OrtAfPl
for b2 being Subset of b1
for b3 being Element of b1 st b2 is_line holds
ex b4 being Subset of b1 st
( b3 in b4 & b2 _|_ b4 )
proof end;

theorem Th4: :: CONMETR:4
for b1 being OrtAfPl
for b2, b3, b4 being Element of b1
for b5 being Subset of b1 st b5 is_line & b2 in b5 & b3 in b5 & b4 in b5 holds
LIN b2,b3,b4
proof end;

theorem Th5: :: CONMETR:5
for b1 being OrtAfPl
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 st b4 is_line & b5 is_line & b2 in b4 & b3 in b4 & b2 in b5 & b3 in b5 & not b2 = b3 holds
b4 = b5
proof end;

theorem Th6: :: CONMETR:6
for b1 being OrtAfPl
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1
for b7 being Subset of (Af b1)
for b8, b9 being Element of (Af b1) st b4 = b8 & b5 = b9 & b6 = b7 & b2 in b6 & b3 in b6 & b8,b9 // b7 holds
b4,b5 // b2,b3
proof end;

theorem Th7: :: CONMETR:7
for b1 being OrtAfPl st TDES_holds_in b1 holds
Af b1 satisfies_TDES
proof end;

theorem Th8: :: CONMETR:8
for b1 being OrtAfPl st Af b1 satisfies_des holds
des_holds_in b1
proof end;

theorem Th9: :: CONMETR:9
for b1 being OrtAfPl st MH1_holds_in b1 holds
OSCH_holds_in b1
proof end;

theorem Th10: :: CONMETR:10
for b1 being OrtAfPl st MH2_holds_in b1 holds
OSCH_holds_in b1
proof end;

theorem Th11: :: CONMETR:11
for b1 being OrtAfPl st AH_holds_in b1 holds
TDES_holds_in b1
proof end;

theorem Th12: :: CONMETR:12
for b1 being OrtAfPl st OSCH_holds_in b1 & TDES_holds_in b1 holds
SCH_holds_in b1
proof end;

theorem Th13: :: CONMETR:13
for b1 being OrtAfPl st OPAP_holds_in b1 & DES_holds_in b1 holds
PAP_holds_in b1
proof end;

theorem Th14: :: CONMETR:14
for b1 being OrtAfPl st MH1_holds_in b1 & MH2_holds_in b1 holds
OPAP_holds_in b1
proof end;

theorem Th15: :: CONMETR:15
for b1 being OrtAfPl st 3H_holds_in b1 holds
OPAP_holds_in b1
proof end;