:: AFPROJ semantic presentation

begin

theorem :: AFPROJ:1
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) & X : ( ( ) ( ) Subset of ) = the carrier of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( ) ( non empty non trivial ) set ) holds
X : ( ( ) ( ) Subset of ) is being_plane ;

theorem :: AFPROJ:2
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) & X : ( ( ) ( ) Subset of ) is being_plane holds
X : ( ( ) ( ) Subset of ) = the carrier of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( ) ( non empty non trivial ) set ) ;

theorem :: AFPROJ:3
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of ) st AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) & X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane holds
X : ( ( ) ( ) Subset of ) = Y : ( ( ) ( ) Subset of ) ;

theorem :: AFPROJ:4
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) = the carrier of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( ) ( non empty non trivial ) set ) & X : ( ( ) ( ) Subset of ) is being_plane holds
AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) ;

theorem :: AFPROJ:5
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for A, K, X, Y being ( ( ) ( ) Subset of ) st not A : ( ( ) ( ) Subset of ) // K : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) & K : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) & K : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) is being_line & K : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane holds
X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ;

theorem :: AFPROJ:6
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X, A, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & A : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) holds
A : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func AfLines AS -> ( ( ) ( ) Subset-Family of ) equals :: AFPROJ:def 1
 { A : ( ( ) ( ) Subset of ) where A is ( ( ) ( ) Subset of ) : A : ( ( ) ( ) Subset of ) is being_line } ;
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func AfPlanes AS -> ( ( ) ( ) Subset-Family of ) equals :: AFPROJ:def 2
 { A : ( ( ) ( ) Subset of ) where A is ( ( ) ( ) Subset of ) : A : ( ( ) ( ) Subset of ) is being_plane } ;
end;

theorem :: AFPROJ:7
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in AfLines AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( ) ( ) Subset-Family of ) iff ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is being_line ) ) ;

theorem :: AFPROJ:8
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in AfPlanes AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( ) ( ) Subset-Family of ) iff ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) is being_plane ) ) ;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func LinesParallelity AS -> ( ( symmetric transitive V28( AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) ( Relation-like AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -defined AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -valued symmetric transitive V28( AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) Equivalence_Relation of AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) equals :: AFPROJ:def 3
 { [K : ( ( ) ( ) Subset of ) ,M : ( ( ) ( ) Subset of ) ] : ( ( ) ( V1() ) Element of [:(bool the carrier of AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(bool the carrier of AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) where K, M is ( ( ) ( ) Subset of ) : ( K : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) is being_line & K : ( ( ) ( ) Subset of ) '||' M : ( ( ) ( ) Subset of ) ) } ;
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func PlanesParallelity AS -> ( ( symmetric transitive V28( AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) ( Relation-like AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -defined AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -valued symmetric transitive V28( AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) Equivalence_Relation of AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) equals :: AFPROJ:def 4
 { [X : ( ( ) ( ) Subset of ) ,Y : ( ( ) ( ) Subset of ) ] : ( ( ) ( V1() ) Element of [:(bool the carrier of AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ,(bool the carrier of AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) where X, Y is ( ( ) ( ) Subset of ) : ( X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ) } ;
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
let X be ( ( ) ( ) Subset of ) ;
func LDir X -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: AFPROJ:def 5
 Class ((LinesParallelity AS : ( ( ) ( ) IncStruct ) ) : ( ( symmetric transitive V28( AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) ( Relation-like AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -defined AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -valued symmetric transitive V28( AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) Equivalence_Relation of AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ,X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (AfLines AS : ( ( ) ( ) IncStruct ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
let X be ( ( ) ( ) Subset of ) ;
func PDir X -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) equals :: AFPROJ:def 6
 Class ((PlanesParallelity AS : ( ( ) ( ) IncStruct ) ) : ( ( symmetric transitive V28( AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) ( Relation-like AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -defined AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -valued symmetric transitive V28( AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) Equivalence_Relation of AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ,X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (AfPlanes AS : ( ( ) ( ) IncStruct ) ) : ( ( ) ( ) Subset-Family of ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: AFPROJ:9
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_line holds
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ex Y being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = Y : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ) ) ;

theorem :: AFPROJ:10
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane holds
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in PDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff ex Y being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = Y : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ) ) ;

theorem :: AFPROJ:11
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_line & Y : ( ( ) ( ) Subset of ) is being_line holds
( LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = LDir Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff X : ( ( ) ( ) Subset of ) // Y : ( ( ) ( ) Subset of ) ) ;

theorem :: AFPROJ:12
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_line & Y : ( ( ) ( ) Subset of ) is being_line holds
( LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = LDir Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ) ;

theorem :: AFPROJ:13
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is being_plane & Y : ( ( ) ( ) Subset of ) is being_plane holds
( PDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = PDir Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) iff X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ) ;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func Dir_of_Lines AS -> ( ( non empty ) ( non empty ) set ) equals :: AFPROJ:def 7
 Class (LinesParallelity AS : ( ( ) ( ) IncStruct ) ) : ( ( symmetric transitive V28( AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) ( Relation-like AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -defined AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -valued symmetric transitive V28( AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) Equivalence_Relation of AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) a_partition of AfLines AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ;
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func Dir_of_Planes AS -> ( ( non empty ) ( non empty ) set ) equals :: AFPROJ:def 8
 Class (PlanesParallelity AS : ( ( ) ( ) IncStruct ) ) : ( ( symmetric transitive V28( AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) ( Relation-like AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -defined AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) -valued symmetric transitive V28( AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ) Equivalence_Relation of AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) a_partition of AfPlanes AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) Subset-Family of ) ) ;
end;

theorem :: AFPROJ:14
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in Dir_of_Lines AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( non empty ) ( non empty ) set ) iff ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset of ) is being_line ) ) ;

theorem :: AFPROJ:15
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in Dir_of_Planes AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( non empty ) ( non empty ) set ) iff ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = PDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset of ) is being_plane ) ) ;

theorem :: AFPROJ:16
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) holds the carrier of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( ) ( non empty non trivial ) set ) misses Dir_of_Lines AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( non empty ) ( non empty ) set ) ;

theorem :: AFPROJ:17
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) st AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) holds
AfLines AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( ) ( ) Subset-Family of ) misses Dir_of_Planes AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( non empty ) ( non empty ) set ) ;

theorem :: AFPROJ:18
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in [:(AfLines AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( ) ( ) Subset-Family of ) ,{1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) iff ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = [X : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & X : ( ( ) ( ) Subset of ) is being_line ) ) ;

theorem :: AFPROJ:19
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in [:(Dir_of_Planes AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( non empty ) ( non empty ) set ) ,{2 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) iff ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = [(PDir X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & X : ( ( ) ( ) Subset of ) is being_plane ) ) ;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func ProjectivePoints AS -> ( ( non empty ) ( non empty ) set ) equals :: AFPROJ:def 9
 the carrier of AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) set ) \/ (Dir_of_Lines AS : ( ( ) ( ) IncStruct ) ) : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ;
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func ProjectiveLines AS -> ( ( non empty ) ( non empty ) set ) equals :: AFPROJ:def 10
[:(AfLines AS : ( ( ) ( ) IncStruct ) ) : ( ( ) ( ) Subset-Family of ) ,{1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) \/ [:(Dir_of_Planes AS : ( ( ) ( ) IncStruct ) ) : ( ( non empty ) ( non empty ) set ) ,{2 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ;
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func Proj_Inc AS -> ( ( ) ( Relation-like ProjectivePoints AS : ( ( ) ( ) IncStruct ) : ( ( non empty ) ( non empty ) set ) -defined ProjectiveLines AS : ( ( ) ( ) IncStruct ) : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ,) means :: AFPROJ:def 11
 for x, y being ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V1() ) set ) in it : ( ( non empty ) ( non empty ) set ) iff ( ex K being ( ( ) ( ) Subset of ) st
( K : ( ( ) ( ) Subset of ) is being_line & y : ( ( ) ( ) set ) = [K : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & ( ( x : ( ( ) ( ) set ) in the carrier of AS : ( ( ) ( ) IncStruct ) : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in K : ( ( ) ( ) Subset of ) ) or x : ( ( ) ( ) set ) = LDir K : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ) or ex K, X being ( ( ) ( ) Subset of ) st
( K : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane & x : ( ( ) ( ) set ) = LDir K : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) set ) = [(PDir X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & K : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) ) ) );
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func Inc_of_Dir AS -> ( ( ) ( Relation-like Dir_of_Lines AS : ( ( ) ( ) IncStruct ) : ( ( non empty ) ( non empty ) set ) -defined Dir_of_Planes AS : ( ( ) ( ) IncStruct ) : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ,) means :: AFPROJ:def 12
 for x, y being ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( V1() ) set ) in it : ( ( non empty ) ( non empty ) set ) iff ex A, X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = LDir A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) set ) = PDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane & A : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) ) );
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func IncProjSp_of AS -> ( ( strict ) ( strict ) IncProjStr ) equals :: AFPROJ:def 13
 IncProjStr(# (ProjectivePoints AS : ( ( ) ( ) IncStruct ) ) : ( ( non empty ) ( non empty ) set ) ,(ProjectiveLines AS : ( ( ) ( ) IncStruct ) ) : ( ( non empty ) ( non empty ) set ) ,(Proj_Inc AS : ( ( ) ( ) IncStruct ) ) : ( ( ) ( Relation-like ProjectivePoints AS : ( ( ) ( ) IncStruct ) : ( ( non empty ) ( non empty ) set ) -defined ProjectiveLines AS : ( ( ) ( ) IncStruct ) : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ,) #) : ( ( strict ) ( strict ) IncProjStr ) ;
end;

definition
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
func ProjHorizon AS -> ( ( strict ) ( strict ) IncProjStr ) equals :: AFPROJ:def 14
 IncProjStr(# (Dir_of_Lines AS : ( ( ) ( ) IncStruct ) ) : ( ( non empty ) ( non empty ) set ) ,(Dir_of_Planes AS : ( ( ) ( ) IncStruct ) ) : ( ( non empty ) ( non empty ) set ) ,(Inc_of_Dir AS : ( ( ) ( ) IncStruct ) ) : ( ( ) ( Relation-like Dir_of_Lines AS : ( ( ) ( ) IncStruct ) : ( ( non empty ) ( non empty ) set ) -defined Dir_of_Planes AS : ( ( ) ( ) IncStruct ) : ( ( non empty ) ( non empty ) set ) -valued ) Relation of ,) #) : ( ( strict ) ( strict ) IncProjStr ) ;
end;

theorem :: AFPROJ:20
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) iff ( x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset of ) is being_line ) ) ) ;

theorem :: AFPROJ:21
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) iff ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset of ) is being_line ) ) ;

theorem :: AFPROJ:22
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) is ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) holds
x : ( ( ) ( ) set ) is ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ;

theorem :: AFPROJ:23
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) iff ex X being ( ( ) ( ) Subset of ) st
( ( x : ( ( ) ( ) set ) = [X : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & X : ( ( ) ( ) Subset of ) is being_line ) or ( x : ( ( ) ( ) set ) = [(PDir X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & X : ( ( ) ( ) Subset of ) is being_plane ) ) ) ;

theorem :: AFPROJ:24
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) iff ex X being ( ( ) ( ) Subset of ) st
( x : ( ( ) ( ) set ) = PDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset of ) is being_plane ) ) ;

theorem :: AFPROJ:25
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) is ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) holds
[x : ( ( ) ( ) set ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) is ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) ;

theorem :: AFPROJ:26
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) )
for X being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) & [X : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) = A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) iff ( X : ( ( ) ( ) Subset of ) is being_line & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in X : ( ( ) ( ) Subset of ) ) ) ;

theorem :: AFPROJ:27
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) )
for X being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) & [(PDir X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) = A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) holds
not a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) ;

theorem :: AFPROJ:28
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for Y, X being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) = LDir Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & [X : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) = A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) & Y : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_line holds
( a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) iff Y : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) ) ;

theorem :: AFPROJ:29
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for Y, X being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) = LDir Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [(PDir X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & Y : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) is being_plane holds
( a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) iff Y : ( ( ) ( ) Subset of ) '||' X : ( ( ) ( ) Subset of ) ) ;

theorem :: AFPROJ:30
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ) is being_line & a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) = LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [X : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) holds
a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) ;

theorem :: AFPROJ:31
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ) is being_line & Y : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) = LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [(PDir Y : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) holds
a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) ;

theorem :: AFPROJ:32
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for Y, X, X9 being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st Y : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & X9 : ( ( ) ( ) Subset of ) // X : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) = LDir X9 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [(PDir Y : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) holds
a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) ;

theorem :: AFPROJ:33
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [(PDir X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & X : ( ( ) ( ) Subset of ) is being_plane & a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) holds
not a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFPROJ:34
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of )
for p being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [X : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & X : ( ( ) ( ) Subset of ) is being_line & p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) & p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) is not ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) = LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: AFPROJ:35
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X being ( ( ) ( ) Subset of )
for p, a being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [X : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & X : ( ( ) ( ) Subset of ) is being_line & p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) <> p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) & p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) is not ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFPROJ:36
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for X, Y being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) = LDir X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) = PDir Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset of ) is being_line & Y : ( ( ) ( ) Subset of ) is being_plane holds
( a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) iff X : ( ( ) ( ) Subset of ) '||' Y : ( ( ) ( ) Subset of ) ) ;

theorem :: AFPROJ:37
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for a being ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) )
for a9 being ( ( ) ( ) Element of the Points of (IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) )
for A being ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) )
for A9 being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st a9 : ( ( ) ( ) Element of the Points of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & A9 : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) holds
( a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) iff a9 : ( ( ) ( ) Element of the Points of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A9 : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: AFPROJ:38
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for a, b being ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) )
for A, K being ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on K : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on K : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & not a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) holds
A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) = K : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: AFPROJ:39
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for A being ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ex a, b, c being ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) <> c : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) <> a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: AFPROJ:40
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for a, b being ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ex A being ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on A : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: AFPROJ:41
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x, y being ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) )
for X being ( ( ) ( ) Element of the Lines of (IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & [x : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ,X : ( ( ) ( ) Element of the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( V1() ) Element of [: the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) , the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) in the Inc of (IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( ) ( Relation-like the Points of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) -defined the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [: the Points of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) , the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & [y : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ,X : ( ( ) ( ) Element of the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ] : ( ( ) ( V1() ) Element of [: the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) , the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) in the Inc of (IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( ) ( Relation-like the Points of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) -defined the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [: the Points of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) , the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
ex Y being ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st X : ( ( ) ( ) Element of the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) = [Y : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) ;

theorem :: AFPROJ:42
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for x being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) )
for X being ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st [x : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,[X : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ,2 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) ] : ( ( ) ( V1() ) set ) in the Inc of (IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( ) ( Relation-like the Points of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) -defined the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) -valued ) Element of bool [: the Points of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) , the Lines of (IncProjSp_of b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: AFPROJ:43
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for Y, X, X9 being ( ( ) ( ) Subset of )
for P, Q being ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) st Y : ( ( ) ( ) Subset of ) is being_plane & X : ( ( ) ( ) Subset of ) is being_line & X9 : ( ( ) ( ) Subset of ) is being_line & X : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & X9 : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) & P : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [X : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) & Q : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) = [X9 : ( ( ) ( ) Subset of ) ,1 : ( ( ) ( non empty ) set ) ] : ( ( ) ( V1() ) set ) holds
ex q being ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) st
( q : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on P : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) & q : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) on Q : ( ( ) ( ) LINE of ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: AFPROJ:44
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for a, b, c, d, p being ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) )
for M, N, P, Q being ( ( ) ( ) Element of the Lines of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on M : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on M : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on N : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & d : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on N : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on M : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on N : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on P : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on P : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on Q : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & d : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on Q : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & not p : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on P : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & not p : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on Q : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & M : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) <> N : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) holds
ex q being ( ( ) ( ) Element of the Points of (ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) st
( q : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on P : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) & q : ( ( ) ( ) Element of the Points of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) on Q : ( ( ) ( ) Element of the Lines of (ProjHorizon b1 : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ) : ( ( strict ) ( strict ) IncProjStr ) : ( ( non empty ) ( non empty ) set ) ) ) ;

registration
let AS be ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) ;
cluster IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinStruct ) : ( ( strict ) ( strict ) IncProjStr ) -> strict linear partial up-2-dimensional up-3-rank Vebleian ;
end;

registration
cluster strict linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional for ( ( ) ( ) IncProjStr ) ;
end;

registration
let AS be ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) ;
cluster IncProjSp_of AS : ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinStruct ) : ( ( strict ) ( strict linear partial up-2-dimensional up-3-rank Vebleian ) IncProjStr ) -> strict 2-dimensional ;
end;

theorem :: AFPROJ:45
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) st IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( strict ) ( strict linear partial up-2-dimensional up-3-rank Vebleian ) IncProjStr ) is 2-dimensional holds
AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) ;

theorem :: AFPROJ:46
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) st AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is not ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) holds
ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( strict ) ( strict ) IncProjStr ) is ( ( linear partial up-2-dimensional up-3-rank Vebleian ) ( linear partial up-2-dimensional up-3-rank Vebleian ) IncProjSp) ;

theorem :: AFPROJ:47
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) st ProjHorizon AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( strict ) ( strict ) IncProjStr ) is ( ( linear partial up-2-dimensional up-3-rank Vebleian ) ( linear partial up-2-dimensional up-3-rank Vebleian ) IncProjSp) holds
not AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is ( ( non trivial AffinSpace-like 2-dimensional ) ( non empty non trivial AffinSpace-like 2-dimensional ) AffinPlane) ;

theorem :: AFPROJ:48
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for M, N being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st M : ( ( ) ( ) Subset of ) is being_line & N : ( ( ) ( ) Subset of ) is being_line & M : ( ( ) ( ) Subset of ) <> N : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in M : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in N : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> c9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in M : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in M : ( ( ) ( ) Subset of ) & a9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in N : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in N : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in N : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,a9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFPROJ:49
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) st IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( strict ) ( strict linear partial up-2-dimensional up-3-rank Vebleian ) IncProjStr ) is Pappian holds
AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is Pappian ;

theorem :: AFPROJ:50
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace)
for A, P, C being ( ( ) ( ) Subset of )
for o, a, b, c, a9, b9, c9 being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in A : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in P : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in C : ( ( ) ( ) Subset of ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in A : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in P : ( ( ) ( ) Subset of ) & b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in P : ( ( ) ( ) Subset of ) & c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in C : ( ( ) ( ) Subset of ) & c9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in C : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) is being_line & P : ( ( ) ( ) Subset of ) is being_line & C : ( ( ) ( ) Subset of ) is being_line & A : ( ( ) ( ) Subset of ) <> P : ( ( ) ( ) Subset of ) & A : ( ( ) ( ) Subset of ) <> C : ( ( ) ( ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // a9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & ( o : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = a9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) // b9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ,c9 : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: AFPROJ:51
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) st IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( strict ) ( strict linear partial up-2-dimensional up-3-rank Vebleian ) IncProjStr ) is Desarguesian holds
AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is Desarguesian ;

theorem :: AFPROJ:52
for AS being ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) st IncProjSp_of AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) : ( ( strict ) ( strict linear partial up-2-dimensional up-3-rank Vebleian ) IncProjStr ) is Fanoian holds
AS : ( ( non trivial AffinSpace-like ) ( non empty non trivial AffinSpace-like ) AffinSpace) is Fanoian ;