:: PARDEPAP semantic presentation

begin

theorem :: PARDEPAP:1
for SAS being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st SAS : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Pappian holds
for a1, a2, a3, b1, b2, b3 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PARDEPAP:2
for SAS being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st SAS : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is Desarguesian holds
for o, a, a9, b, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PARDEPAP:3
for SAS being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st SAS : ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) is translational holds
for a, a9, b, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PARDEPAP:4
ex SAS being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane) st
( ( for o, a, a9, b, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) & ( for a, a9, b, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) & ( for a1, a2, a3, b1, b2, b3 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
a3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b3 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) & ( for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
not a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ) ;

theorem :: PARDEPAP:5
for SAS being ( ( V46() AffinSpace-like 2-dimensional ) ( V41() V46() AffinSpace-like 2-dimensional ) AffinPlane)
for o, a being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ex p being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
for b, c being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
( o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & ex d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) implies ( o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ) ) ;