let AS be AffinSpace; 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); 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); ( 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)
; 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
; 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; verum