let AS be AffinSpace; :: thesis: for x, y being Element of the Points of (ProjHorizon AS)
for X being Element of the Lines of (IncProjSp_of AS) st x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) holds
ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2]
let x, y be Element of the Points of (ProjHorizon AS); :: thesis: for X being Element of the Lines of (IncProjSp_of AS) st x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) holds
ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2]
let X be Element of the Lines of (IncProjSp_of AS); :: thesis: ( x <> y & [x,X] in the Inc of (IncProjSp_of AS) & [y,X] in the Inc of (IncProjSp_of AS) implies ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2] )
reconsider a = x, b = y as POINT of (IncProjSp_of AS) by Th22;
assume that
A1: x <> y and
A2: [x,X] in the Inc of (IncProjSp_of AS) and
A3: [y,X] in the Inc of (IncProjSp_of AS) ; :: thesis: ex Y being Element of the Lines of (ProjHorizon AS) st X = [Y,2]
A4: b on X by A3, INCSP_1:def 1;
consider Y being Element of the Lines of (ProjHorizon AS) such that
A5: x on Y and
A6: y on Y by Th40;
reconsider A = [Y,2] as LINE of (IncProjSp_of AS) by Th25;
consider Z being Subset of AS such that
A7: Y = PDir Z and
A8: Z is being_plane by Th15;
consider X2 being Subset of AS such that
A9: y = LDir X2 and
A10: X2 is being_line by Th14;
X2 '||' Z by A9, A10, A6, A7, A8, Th36;
then A11: b on A by A9, A10, A7, A8, Th29;
take Y ; :: thesis: X = [Y,2]
consider X1 being Subset of AS such that
A12: x = LDir X1 and
A13: X1 is being_line by Th14;
X1 '||' Z by A12, A13, A5, A7, A8, Th36;
then A14: a on A by A12, A13, A7, A8, Th29;
a on X by A2, INCSP_1:def 1;
hence X = [Y,2] by A1, A4, A14, A11, Lm2; :: thesis: verum