:: PROJRED1 semantic presentation

begin

theorem :: PROJRED1:1
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
not for a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:2
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
not for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:3
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
ex a, b being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJRED1:4
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a, b being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
ex A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJRED1:5
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex A, B, C being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJRED1:6
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex a being ( ( ) ( ) POINT 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 B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJRED1:7
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:8
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a, b being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJRED1:9
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a, b being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex A 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 A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJRED1:10
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for o, a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B, P, Q being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:11
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJRED1:12
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp)
for o, b1, a1, b2, a2, b3, a3, r, s, t being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,t : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {t : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on B1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on B2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on B3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & C1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C3 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_mutually_different & o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
ex O being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,t : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on O : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:13
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) st ex A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) are_mutually_different ) holds
for B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex p, q, r, s being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) are_mutually_different ) ;

theorem :: PROJRED1:14
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) ex p, q, r, s, a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex A, B, C, Q, L, R, S, D being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st
( not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on S : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on S : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on S : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJRED1:15
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) ex a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex A, B, C, D being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on D : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,C : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,D : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_mutually_different ) ;

theorem :: PROJRED1:16
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp) ex a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) are_mutually_different ) ;

theorem :: PROJRED1:17
for IPP being ( ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) ( V22() partial up-2-dimensional up-3-rank V73() Fanoian ) IncProjSp)
for B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex p, q, r, s being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) are_mutually_different ) ;

definition
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) ;
let K, L be ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
let p be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
assume that
not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) and
not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
func IncProj (K,p,L) -> ( ( Function-like ) ( Relation-like the Points of IPP : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) -defined the Points of IPP : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) PartFunc of ,) means :: PROJRED1:def 1
( dom it : ( ( ) ( Relation-like IPP : ( ( ) ( ) IncStruct ) -defined L : ( ( V4() ) ( V4() ) set ) -valued ) Element of bool [:IPP : ( ( ) ( ) IncStruct ) ,L : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the Points of IPP : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) c= the Points of IPP : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) & ( for x being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) in dom it : ( ( ) ( Relation-like IPP : ( ( ) ( ) IncStruct ) -defined L : ( ( V4() ) ( V4() ) set ) -valued ) Element of bool [:IPP : ( ( ) ( ) IncStruct ) ,L : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool the Points of IPP : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) iff x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( V4() ) ( V4() ) set ) ) ) & ( for x, y being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( V4() ) ( V4() ) set ) & y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( V4() ) ( V4() ) set ) holds
( it : ( ( ) ( Relation-like IPP : ( ( ) ( ) IncStruct ) -defined L : ( ( V4() ) ( V4() ) set ) -valued ) Element of bool [:IPP : ( ( ) ( ) IncStruct ) ,L : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) set ) = y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) iff ex X being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st
( p : ( ( ) ( Relation-like IPP : ( ( ) ( ) IncStruct ) -defined K : ( ( V4() ) ( V4() ) set ) -valued ) Element of bool [:IPP : ( ( ) ( ) IncStruct ) ,K : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) on X : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on X : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on X : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ) ) );
end;

theorem :: PROJRED1:18
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 p being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for K being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
for x being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
(IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) . x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) set ) = x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:19
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 p, x being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for K, L being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
(IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) . x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) set ) is ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:20
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 p, x, y being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for K, L being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) . x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) set ) holds
y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:21
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 p, y being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for K, L being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) in rng (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) : ( ( ) ( ) set ) holds
y : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:22
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 p, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for K, L, R being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( dom ((IncProj (L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) * (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = dom (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) : ( ( ) ( ) Element of bool the Points of b1 : ( ( 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 ) ) & rng ((IncProj (L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) * (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = rng (IncProj (L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) : ( ( ) ( ) set ) ) ;

theorem :: PROJRED1:23
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 p being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for K, L being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) )
for a1, b1, a2, b2 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) . a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) set ) = a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) . b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) set ) = b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:24
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 p, x being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for K, L being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
(IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) . x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) set ) = x : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJRED1:25
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 p, q, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for K, L, R being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
ex o being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & (IncProj (L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) * (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) : ( ( Relation-like ) ( Relation-like Function-like ) set ) = IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( 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 b1 : ( ( 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 ) PartFunc of ,) ) ;