:: AFF_3 semantic presentation

definition
let c1 be AffinPlane;
attr a1 is satisfying_DES1 means :Def1: :: AFF_3:def 1
for b1, b2, b3 being Subset of a1
for b4, b5, b6, b7, b8, b9, b10, b11, b12 being Element of a1 st b1 is_line & b2 is_line & b3 is_line & b2 <> b1 & b2 <> b3 & b1 <> b3 & b4 in b1 & b5 in b1 & b6 in b1 & b4 in b2 & b7 in b2 & b8 in b2 & b4 in b3 & b9 in b3 & b10 in b3 & b4 <> b5 & b4 <> b7 & b4 <> b9 & b11 <> b12 & not LIN b7,b5,b9 & not LIN b8,b6,b10 & b5 <> b6 & LIN b7,b5,b11 & LIN b8,b6,b11 & LIN b7,b9,b12 & LIN b8,b10,b12 & b5,b9 // b6,b10 holds
b5,b9 // b11,b12;
end;

:: deftheorem Def1 defines satisfying_DES1 AFF_3:def 1 :
for b1 being AffinPlane holds
( b1 is satisfying_DES1 iff for b2, b3, b4 being Subset of b1
for b5, b6, b7, b8, b9, b10, b11, b12, b13 being Element of b1 st b2 is_line & b3 is_line & b4 is_line & b3 <> b2 & b3 <> b4 & b2 <> b4 & b5 in b2 & b6 in b2 & b7 in b2 & b5 in b3 & b8 in b3 & b9 in b3 & b5 in b4 & b10 in b4 & b11 in b4 & b5 <> b6 & b5 <> b8 & b5 <> b10 & b12 <> b13 & not LIN b8,b6,b10 & not LIN b9,b7,b11 & b6 <> b7 & LIN b8,b6,b12 & LIN b9,b7,b12 & LIN b8,b10,b13 & LIN b9,b11,b13 & b6,b10 // b7,b11 holds
b6,b10 // b12,b13 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_DES1 for satisfying_DES1 c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_DES1_1 means :Def2: :: AFF_3:def 2
for b1, b2, b3 being Subset of a1
for b4, b5, b6, b7, b8, b9, b10, b11, b12 being Element of a1 st b1 is_line & b2 is_line & b3 is_line & b2 <> b1 & b2 <> b3 & b1 <> b3 & b4 in b1 & b5 in b1 & b6 in b1 & b4 in b2 & b7 in b2 & b8 in b2 & b4 in b3 & b9 in b3 & b10 in b3 & b4 <> b5 & b4 <> b7 & b4 <> b9 & b11 <> b12 & b9 <> b12 & not LIN b7,b5,b9 & not LIN b8,b6,b10 & LIN b7,b5,b11 & LIN b8,b6,b11 & LIN b7,b9,b12 & LIN b8,b10,b12 & b5,b9 // b11,b12 holds
b5,b9 // b6,b10;
end;

:: deftheorem Def2 defines satisfying_DES1_1 AFF_3:def 2 :
for b1 being AffinPlane holds
( b1 is satisfying_DES1_1 iff for b2, b3, b4 being Subset of b1
for b5, b6, b7, b8, b9, b10, b11, b12, b13 being Element of b1 st b2 is_line & b3 is_line & b4 is_line & b3 <> b2 & b3 <> b4 & b2 <> b4 & b5 in b2 & b6 in b2 & b7 in b2 & b5 in b3 & b8 in b3 & b9 in b3 & b5 in b4 & b10 in b4 & b11 in b4 & b5 <> b6 & b5 <> b8 & b5 <> b10 & b12 <> b13 & b10 <> b13 & not LIN b8,b6,b10 & not LIN b9,b7,b11 & LIN b8,b6,b12 & LIN b9,b7,b12 & LIN b8,b10,b13 & LIN b9,b11,b13 & b6,b10 // b12,b13 holds
b6,b10 // b7,b11 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_DES1_1 for satisfying_DES1_1 c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_DES1_2 means :Def3: :: AFF_3:def 3
for b1, b2, b3 being Subset of a1
for b4, b5, b6, b7, b8, b9, b10, b11, b12 being Element of a1 st b1 is_line & b2 is_line & b3 is_line & b2 <> b1 & b2 <> b3 & b1 <> b3 & b4 in b1 & b5 in b1 & b6 in b1 & b4 in b2 & b7 in b2 & b8 in b2 & b9 in b3 & b10 in b3 & b4 <> b5 & b4 <> b7 & b4 <> b9 & b11 <> b12 & not LIN b7,b5,b9 & not LIN b8,b6,b10 & b9 <> b10 & LIN b7,b5,b11 & LIN b8,b6,b11 & LIN b7,b9,b12 & LIN b8,b10,b12 & b5,b9 // b6,b10 & b5,b9 // b11,b12 holds
b4 in b3;
end;

:: deftheorem Def3 defines satisfying_DES1_2 AFF_3:def 3 :
for b1 being AffinPlane holds
( b1 is satisfying_DES1_2 iff for b2, b3, b4 being Subset of b1
for b5, b6, b7, b8, b9, b10, b11, b12, b13 being Element of b1 st b2 is_line & b3 is_line & b4 is_line & b3 <> b2 & b3 <> b4 & b2 <> b4 & b5 in b2 & b6 in b2 & b7 in b2 & b5 in b3 & b8 in b3 & b9 in b3 & b10 in b4 & b11 in b4 & b5 <> b6 & b5 <> b8 & b5 <> b10 & b12 <> b13 & not LIN b8,b6,b10 & not LIN b9,b7,b11 & b10 <> b11 & LIN b8,b6,b12 & LIN b9,b7,b12 & LIN b8,b10,b13 & LIN b9,b11,b13 & b6,b10 // b7,b11 & b6,b10 // b12,b13 holds
b5 in b4 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_DES1_2 for satisfying_DES1_2 c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_DES1_3 means :Def4: :: AFF_3:def 4
for b1, b2, b3 being Subset of a1
for b4, b5, b6, b7, b8, b9, b10, b11, b12 being Element of a1 st b1 is_line & b2 is_line & b3 is_line & b2 <> b1 & b2 <> b3 & b1 <> b3 & b4 in b1 & b5 in b1 & b6 in b1 & b7 in b2 & b8 in b2 & b4 in b3 & b9 in b3 & b10 in b3 & b4 <> b5 & b4 <> b7 & b4 <> b9 & b11 <> b12 & not LIN b7,b5,b9 & not LIN b8,b6,b10 & b7 <> b8 & b5 <> b6 & LIN b7,b5,b11 & LIN b8,b6,b11 & LIN b7,b9,b12 & LIN b8,b10,b12 & b5,b9 // b6,b10 & b5,b9 // b11,b12 holds
b4 in b2;
end;

:: deftheorem Def4 defines satisfying_DES1_3 AFF_3:def 4 :
for b1 being AffinPlane holds
( b1 is satisfying_DES1_3 iff for b2, b3, b4 being Subset of b1
for b5, b6, b7, b8, b9, b10, b11, b12, b13 being Element of b1 st b2 is_line & b3 is_line & b4 is_line & b3 <> b2 & b3 <> b4 & b2 <> b4 & b5 in b2 & b6 in b2 & b7 in b2 & b8 in b3 & b9 in b3 & b5 in b4 & b10 in b4 & b11 in b4 & b5 <> b6 & b5 <> b8 & b5 <> b10 & b12 <> b13 & not LIN b8,b6,b10 & not LIN b9,b7,b11 & b8 <> b9 & b6 <> b7 & LIN b8,b6,b12 & LIN b9,b7,b12 & LIN b8,b10,b13 & LIN b9,b11,b13 & b6,b10 // b7,b11 & b6,b10 // b12,b13 holds
b5 in b3 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_DES1_3 for satisfying_DES1_3 c1;
end;

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

:: deftheorem Def5 defines satisfying_DES2 AFF_3:def 5 :
for b1 being AffinPlane holds
( b1 is satisfying_DES2 iff for b2, b3, b4 being Subset of b1
for b5, b6, b7, b8, b9, b10, b11, b12 being Element of b1 st b2 is_line & b3 is_line & b4 is_line & b2 <> b3 & b2 <> b4 & b3 <> b4 & b5 in b2 & b6 in b2 & b7 in b3 & b8 in b3 & b9 in b4 & b10 in b4 & b2 // b3 & b2 // b4 & not LIN b7,b5,b9 & not LIN b8,b6,b10 & b11 <> b12 & b5 <> b6 & LIN b7,b5,b11 & LIN b8,b6,b11 & LIN b7,b9,b12 & LIN b8,b10,b12 & b5,b9 // b6,b10 holds
b5,b9 // b11,b12 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_DES2 for satisfying_DES2 c1;
end;

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

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

notation
let c1 be AffinPlane;
synonym c1 satisfies_DES2_1 for satisfying_DES2_1 c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_DES2_2 means :Def7: :: AFF_3:def 7
for b1, b2, b3 being Subset of a1
for b4, b5, b6, b7, b8, b9, b10, b11 being Element of a1 st b1 is_line & b2 is_line & b3 is_line & b1 <> b2 & b1 <> b3 & b2 <> b3 & b4 in b1 & b5 in b1 & b6 in b2 & b7 in b2 & b8 in b3 & b9 in b3 & b1 // b3 & not LIN b6,b4,b8 & not LIN b7,b5,b9 & b10 <> b11 & b4 <> b5 & LIN b6,b4,b10 & LIN b7,b5,b10 & LIN b6,b8,b11 & LIN b7,b9,b11 & b4,b8 // b5,b9 & b4,b8 // b10,b11 holds
b1 // b2;
end;

:: deftheorem Def7 defines satisfying_DES2_2 AFF_3:def 7 :
for b1 being AffinPlane holds
( b1 is satisfying_DES2_2 iff for b2, b3, b4 being Subset of b1
for b5, b6, b7, b8, b9, b10, b11, b12 being Element of b1 st b2 is_line & b3 is_line & b4 is_line & b2 <> b3 & b2 <> b4 & b3 <> b4 & b5 in b2 & b6 in b2 & b7 in b3 & b8 in b3 & b9 in b4 & b10 in b4 & b2 // b4 & not LIN b7,b5,b9 & not LIN b8,b6,b10 & b11 <> b12 & b5 <> b6 & LIN b7,b5,b11 & LIN b8,b6,b11 & LIN b7,b9,b12 & LIN b8,b10,b12 & b5,b9 // b6,b10 & b5,b9 // b11,b12 holds
b2 // b3 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_DES2_2 for satisfying_DES2_2 c1;
end;

definition
let c1 be AffinPlane;
attr a1 is satisfying_DES2_3 means :Def8: :: AFF_3:def 8
for b1, b2, b3 being Subset of a1
for b4, b5, b6, b7, b8, b9, b10, b11 being Element of a1 st b1 is_line & b2 is_line & b3 is_line & b1 <> b2 & b1 <> b3 & b2 <> b3 & b4 in b1 & b5 in b1 & b6 in b2 & b7 in b2 & b8 in b3 & b9 in b3 & b1 // b2 & not LIN b6,b4,b8 & not LIN b7,b5,b9 & b10 <> b11 & b8 <> b9 & LIN b6,b4,b10 & LIN b7,b5,b10 & LIN b6,b8,b11 & LIN b7,b9,b11 & b4,b8 // b5,b9 & b4,b8 // b10,b11 holds
b1 // b3;
end;

:: deftheorem Def8 defines satisfying_DES2_3 AFF_3:def 8 :
for b1 being AffinPlane holds
( b1 is satisfying_DES2_3 iff for b2, b3, b4 being Subset of b1
for b5, b6, b7, b8, b9, b10, b11, b12 being Element of b1 st b2 is_line & b3 is_line & b4 is_line & b2 <> b3 & b2 <> b4 & b3 <> b4 & b5 in b2 & b6 in b2 & b7 in b3 & b8 in b3 & b9 in b4 & b10 in b4 & b2 // b3 & not LIN b7,b5,b9 & not LIN b8,b6,b10 & b11 <> b12 & b9 <> b10 & LIN b7,b5,b11 & LIN b8,b6,b11 & LIN b7,b9,b12 & LIN b8,b10,b12 & b5,b9 // b6,b10 & b5,b9 // b11,b12 holds
b2 // b4 );

notation
let c1 be AffinPlane;
synonym c1 satisfies_DES2_3 for satisfying_DES2_3 c1;
end;

theorem Th1: :: AFF_3:1
canceled;

theorem Th2: :: AFF_3:2
canceled;

theorem Th3: :: AFF_3:3
canceled;

theorem Th4: :: AFF_3:4
canceled;

theorem Th5: :: AFF_3:5
canceled;

theorem Th6: :: AFF_3:6
canceled;

theorem Th7: :: AFF_3:7
canceled;

theorem Th8: :: AFF_3:8
canceled;

theorem Th9: :: AFF_3:9
for b1 being AffinPlane st b1 satisfies_DES1 holds
b1 satisfies_DES1_1
proof end;

theorem Th10: :: AFF_3:10
for b1 being AffinPlane st b1 satisfies_DES1_1 holds
b1 satisfies_DES1
proof end;

theorem Th11: :: AFF_3:11
for b1 being AffinPlane st b1 satisfies_DES holds
b1 satisfies_DES1
proof end;

theorem Th12: :: AFF_3:12
for b1 being AffinPlane st b1 satisfies_DES holds
b1 satisfies_DES1_2
proof end;

theorem Th13: :: AFF_3:13
for b1 being AffinPlane st b1 satisfies_DES1_2 holds
b1 satisfies_DES1_3
proof end;

theorem Th14: :: AFF_3:14
for b1 being AffinPlane st b1 satisfies_DES1_2 holds
b1 satisfies_DES
proof end;

theorem Th15: :: AFF_3:15
for b1 being AffinPlane st b1 satisfies_DES2_1 holds
b1 satisfies_DES2
proof end;

theorem Th16: :: AFF_3:16
for b1 being AffinPlane holds
( b1 satisfies_DES2_1 iff b1 satisfies_DES2_3 )
proof end;

theorem Th17: :: AFF_3:17
for b1 being AffinPlane holds
( b1 satisfies_DES2 iff b1 satisfies_DES2_2 )
proof end;

theorem Th18: :: AFF_3:18
for b1 being AffinPlane st b1 satisfies_DES1_3 holds
b1 satisfies_DES2_1
proof end;