let AS be AffinSpace; :: thesis: for x being set st x is Element of the Lines of (ProjHorizon AS) holds
[x,2] is LINE of (IncProjSp_of AS)
let x be set ; :: thesis: ( x is Element of the Lines of (ProjHorizon AS) implies [x,2] is LINE of (IncProjSp_of AS) )
assume x is Element of the Lines of (ProjHorizon AS) ; :: thesis: [x,2] is LINE of (IncProjSp_of AS)
then ex X being Subset of AS st
( x = PDir X & X is being_plane ) by Th15;
hence [x,2] is LINE of (IncProjSp_of AS) by Th23; :: thesis: verum