let IPS be ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) ;
let A, B, C be ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

let IPS be ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) ;
let Z be ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

let IPP be ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for A, B, C being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st ( A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) or B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) or C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) holds
A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for A, B, C being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent holds
( A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for o, y being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
ex x being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) set ) = y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for o being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
dom (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) = CHAIN A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for o being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
rng (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = CHAIN B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) )
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in CHAIN A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) iff ex a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( x : ( ( ) ( ) set ) = a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for o being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is one-to-one ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for o being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
(IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = IncProj (B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for f being ( ( ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Projection of IPP : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) ) holds f : ( ( ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Projection of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is ( ( ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Projection of IPP : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for o being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = id (CHAIN A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) : ( ( total ) ( Relation-like CHAIN b₃ : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined CHAIN b₃ : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -valued Function-like one-to-one total ) Element of bool [:(CHAIN b₃ : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ,(CHAIN b₃ : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds id (CHAIN A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) : ( ( total ) ( Relation-like CHAIN b₂ : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -defined CHAIN b₂ : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) -valued Function-like one-to-one total ) Element of bool [:(CHAIN b₂ : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ,(CHAIN b₂ : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is ( ( ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Projection of IPP : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for o being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B, C being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
(IncProj (C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for o1, o2 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for O1, O2, O3 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not o1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
ex o being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & (IncProj (O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (IncProj (O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = IncProj (O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for a, b, c, d, p, q, pp9 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B, C, Q, O, O1, O2, O3 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
(IncProj (C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = (IncProj (Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for a, b, q, c, o, o99, d, o9, oo9 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, C, B, Q, O, O1, O2, O3 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o99 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
(IncProj (C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = (IncProj (Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for a, b, c, p, d, q, pp9 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, C, Q, B, O, O1, O2, O3 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & not B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for a, b, c, o, o99, d, o9, oo9, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, C, B, Q, O, O1, O2, O3 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o99 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for a, b, q, c, p, d, pp9 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, C, B, O, Q, O1, O2, O3 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & not B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,pp9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for a, b, q, c, o, o99, d, o9, oo9 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, C, B, O, Q, O1, O2, O3 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o99 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,o9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,oo9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp)
for a, b being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B, C, Q, O being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_concurrent & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
ex q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & (IncProj (C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = (IncProj (Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (IncProj (A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) Element of bool [: the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) , the Points of b₁ : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ) ;