:: PASCH semantic presentation

begin

definition
let OAS be ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) ;
attr OAS is satisfying_Int_Par_Pasch means :: PASCH:def 1
 for a, b, c, d, p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) 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 ) ) holds
Mid c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let OAS be ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) ;
attr OAS is satisfying_Ext_Par_Pasch means :: PASCH:def 2
 for a, b, c, d, p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) 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 ) ) & not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let OAS be ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) ;
attr OAS is satisfying_Gen_Par_Pasch means :: PASCH:def 3
 for a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) 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 ) ) & Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
Mid a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;
end;

definition
let OAS be ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) ;
attr OAS is satisfying_Ext_Bet_Pasch means :: PASCH:def 4
 for a, b, c, d, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid y : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) );
end;

definition
let OAS be ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) ;
attr OAS is satisfying_Int_Bet_Pasch means :: PASCH:def 5
 for a, b, c, d, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( Mid b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) );
end;

definition
let OAS be ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) ;
attr OAS is Fanoian means :: PASCH:def 6
 for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st 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 ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) );
end;

theorem :: PASCH:1
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for b, p, c, a being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) 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 ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:2
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, b, c, a being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) 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 ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:3
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, b, c, a being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) 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 ) ) ) ;

theorem :: PASCH:4
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, a, b, c, d1, d2 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
d1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = d2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:5
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for a, b, c, d1, d2 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) 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 ) ) ,d1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
d1 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) = d2 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:6
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, b, c, a, d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) 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 ) ) holds
Mid c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:7
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) holds OAS : ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) is satisfying_Int_Par_Pasch ;

theorem :: PASCH:8
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, b, c, a, d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) 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 ) ) & not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:9
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) holds OAS : ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) is satisfying_Ext_Par_Pasch ;

theorem :: PASCH:10
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for a, b, a9, b9, c, c9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) 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 ) ) & Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
Mid a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:11
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) holds OAS : ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) is satisfying_Gen_Par_Pasch ;

theorem :: PASCH:12
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, a, b, a9, b9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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 ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:13
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, a, a9, b, b9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) 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 ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:14
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:15
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, c, b, d, a being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:16
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, d, a, c, b being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:17
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
not Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:18
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, b, c, a being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:19
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, c, b, a being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:20
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, b, c, a being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:21
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:22
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ex x being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:23
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:24
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) holds OAS : ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) is Fanoian ;

theorem :: PASCH:25
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st 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 ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( LIN x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:26
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for a, b, c, d, p being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) '||' c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;

theorem :: PASCH:27
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for a, b, d, x, c being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex y being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid y : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:28
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) holds OAS : ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) is satisfying_Ext_Bet_Pasch ;

theorem :: PASCH:29
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for a, b, d, x, c being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
ex y being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st
( Mid b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & Mid x : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ) ;

theorem :: PASCH:30
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) holds OAS : ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace) is satisfying_Int_Bet_Pasch ;

theorem :: PASCH:31
for OAS being ( ( V46() OAffinSpace-like ) ( V41() V46() OAffinSpace-like ) OAffinSpace)
for p, a, b, p9, a9, b9 being ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) st Mid p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // p9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & not LIN p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & LIN p9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // a : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,p9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) holds
Mid p9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( V4() V5() ) set ) ) ;