:: PARDEPAP semantic presentation

theorem Th1: :: PARDEPAP:1
for b1 being AffinPlane st b1 satisfies_PAP holds
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 // b2,b4 & b5,b6 // b5,b7 & b2,b6 // b3,b5 & b3,b7 // b4,b6 holds
b4,b5 // b2,b7
proof end;

theorem Th2: :: PARDEPAP:2
for b1 being AffinPlane st b1 satisfies_DES holds
for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st not b2,b3 // b2,b5 & not b2,b3 // b2,b7 & b2,b3 // b2,b4 & b2,b5 // b2,b6 & b2,b7 // b2,b8 & b3,b5 // b4,b6 & b3,b7 // b4,b8 holds
b5,b7 // b6,b8
proof end;

theorem Th3: :: PARDEPAP:3
for b1 being AffinPlane st b1 satisfies_des holds
for b2, b3, b4, b5, b6, b7 being Element of b1 st not b2,b3 // b2,b4 & not b2,b3 // b2,b6 & b2,b3 // b4,b5 & b2,b3 // b6,b7 & b2,b4 // b3,b5 & b2,b6 // b3,b7 holds
b4,b6 // b5,b7
proof end;

theorem Th4: :: PARDEPAP:4
canceled;

theorem Th5: :: PARDEPAP:5
ex b1 being AffinPlane st
( ( for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st not b2,b3 // b2,b5 & not b2,b3 // b2,b7 & b2,b3 // b2,b4 & b2,b5 // b2,b6 & b2,b7 // b2,b8 & b3,b5 // b4,b6 & b3,b7 // b4,b8 holds
b5,b7 // b6,b8 ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 st not b2,b3 // b2,b4 & not b2,b3 // b2,b6 & b2,b3 // b4,b5 & b2,b3 // b6,b7 & b2,b4 // b3,b5 & b2,b6 // b3,b7 holds
b4,b6 // b5,b7 ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 // b2,b4 & b5,b6 // b5,b7 & b2,b6 // b3,b5 & b3,b7 // b4,b6 holds
b4,b5 // b2,b7 ) & ( for b2, b3, b4, b5 being Element of b1 st not b2,b3 // b2,b4 & b2,b3 // b4,b5 & b2,b4 // b3,b5 holds
not b2,b5 // b3,b4 ) )
proof end;

theorem Th6: :: PARDEPAP:6
for b1 being AffinPlane
for b2, b3 being Element of b1 ex b4 being Element of b1 st
for b5, b6 being Element of b1 holds
( b2,b3 // b2,b4 & ex b7 being Element of b1 st
( b2,b4 // b2,b5 implies ( b2,b6 // b2,b7 & b4,b6 // b5,b7 ) ) )
proof end;