let AS be AffinSpace; for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )
let a, b be Element of the Points of (ProjHorizon AS); ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )
consider X being Subset of AS such that
A1:
a = LDir X
and
A2:
X is being_line
by Th14;
consider X9 being Subset of AS such that
A3:
b = LDir X9
and
A4:
X9 is being_line
by Th14;
consider x, y being Element of AS such that
A5:
x in X9
and
y in X9
and
x <> y
by A4, AFF_1:19;
A6:
x in x * X
by A2, AFF_4:def 3;
x * X is being_line
by A2, AFF_4:27;
then consider Z being Subset of AS such that
A7:
X9 c= Z
and
A8:
x * X c= Z
and
A9:
Z is being_plane
by A4, A5, A6, AFF_4:38;
A10:
X9 '||' Z
by A4, A7, A9, AFF_4:42;
reconsider A = PDir Z as Element of the Lines of (ProjHorizon AS) by A9, Th15;
take
A
; ( a on A & b on A )
X // x * X
by A2, AFF_4:def 3;
then
X '||' Z
by A2, A8, A9, AFF_4:41;
hence
( a on A & b on A )
by A1, A2, A3, A4, A9, A10, Th36; verum