:: PROJDES1 semantic presentation

begin

theorem :: PROJDES1:1
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
( b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ) ;

theorem :: PROJDES1:2
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for p being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not for q, r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: PROJDES1:3
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, b9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: PROJDES1:4
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: PROJDES1:5
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for o, a, d, d9, a9, s being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

definition
let FCPS be ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace) ;
let a, b, c, d be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
pred a,b,c,d are_coplanar means :: PROJDES1:def 1
 ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,d : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear );
end;

theorem :: PROJDES1:6
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st ( a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear or b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear or c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear or d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ) holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:7
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar holds
( b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ) ;

theorem :: PROJDES1:8
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar holds
p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:9
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for p, q, r, a, b, c, s being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:10
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for p, q, r, a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:11
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, p, q, r, s being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar holds
ex x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ) ;

theorem :: PROJDES1:12
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace) holds
not for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:13
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for p, q, r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
ex s being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:14
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st ( a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) or d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:15
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, o, a9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:16
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, a9, b9, c9, p, q, r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & not a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar holds
p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: PROJDES1:17
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, a9, o, b, c, b9, c9, p, q, r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & not a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: PROJDES1:18
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, d, o being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear holds
not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ;

theorem :: PROJDES1:19
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, o, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( not a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & not a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar ) ;

theorem :: PROJDES1:20
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for a, b, c, o, d, d9, a9, b9, s, t, u being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & not a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) are_coplanar & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> d9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
not s : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,t : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

definition
let FCPS be ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace) ;
let o, a, b, c be ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
pred o,a,b,c constitute_a_quadrangle means :: PROJDES1:def 2
( not a : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) is_collinear & not o : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,a : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) is_collinear & not o : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,b : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) is_collinear & not o : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,c : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) ,a : ( ( ) ( ) M2( the U1 of FCPS : ( ( V38() V101() V102() ) ( V38() V101() V102() ) L13()) : ( ( ) ( ) set ) )) is_collinear );
end;

theorem :: PROJDES1:21
for FCPS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace)
for o, a, b, c, a9, b9, c9, p, r, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c9 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
r : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( ) set ) ) is_collinear ;

theorem :: PROJDES1:22
for CS being ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace) holds CS : ( ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) ( V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional ) CollProjectiveSpace) is Desarguesian ;

registration
cluster V38() V101() V102() proper Vebleian at_least_3rank up-3-dimensional -> V38() V101() V102() proper Vebleian at_least_3rank Desarguesian up-3-dimensional for ( ( ) ( ) L13()) ;
end;