let AS be AffinSpace; :: thesis: for x being set st x is Element of the Points of (ProjHorizon AS) holds
x is POINT of (IncProjSp_of AS)
let x be set ; :: thesis: ( x is Element of the Points of (ProjHorizon AS) implies x is POINT of (IncProjSp_of AS) )
assume x is Element of the Points of (ProjHorizon AS) ; :: thesis: x is POINT of (IncProjSp_of AS)
then ex X being Subset of AS st
( x = LDir X & X is being_line ) by Th14;
hence x is POINT of (IncProjSp_of AS) by Th20; :: thesis: verum