let AS be AffinSpace; :: thesis: for x being POINT of (IncProjSp_of AS)
for X being Element of the Lines of (ProjHorizon AS) st [x,[X,2]] in the Inc of (IncProjSp_of AS) holds
x is Element of the Points of (ProjHorizon AS)
let x be POINT of (IncProjSp_of AS); :: thesis: for X being Element of the Lines of (ProjHorizon AS) st [x,[X,2]] in the Inc of (IncProjSp_of AS) holds
x is Element of the Points of (ProjHorizon AS)
let X be Element of the Lines of (ProjHorizon AS); :: thesis: ( [x,[X,2]] in the Inc of (IncProjSp_of AS) implies x is Element of the Points of (ProjHorizon AS) )
assume A1: [x,[X,2]] in the Inc of (IncProjSp_of AS) ; :: thesis: x is Element of the Points of (ProjHorizon AS)
reconsider A = [X,2] as LINE of (IncProjSp_of AS) by Th25;
A2: ex Y being Subset of AS st
( X = PDir Y & Y is being_plane ) by Th15;
x is not Element of AS
proof
assume x is Element of AS ; :: thesis: contradiction
then reconsider a = x as Element of AS ;
A3: a = x ;
x on A by A1, INCSP_1:def 1;
hence contradiction by A2, A3, Th27; :: thesis: verum
end;
then ex Y9 being Subset of AS st
( x = LDir Y9 & Y9 is being_line ) by Th20;
hence x is Element of the Points of (ProjHorizon AS) by Th14; :: thesis: verum