let AS be AffinSpace; for a, b being Element of the Points of (ProjHorizon AS)
for A, K being Element of the Lines of (ProjHorizon AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let a, b be Element of the Points of (ProjHorizon AS); for A, K being Element of the Lines of (ProjHorizon AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let A, K be Element of the Lines of (ProjHorizon AS); ( a on A & a on K & b on A & b on K & not a = b implies A = K )
assume that
A1:
a on A
and
A2:
a on K
and
A3:
b on A
and
A4:
b on K
; ( a = b or A = K )
consider Y9 being Subset of AS such that
A5:
b = LDir Y9
and
A6:
Y9 is being_line
by Th14;
consider X9 being Subset of AS such that
A7:
K = PDir X9
and
A8:
X9 is being_plane
by Th15;
A9:
Y9 '||' X9
by A4, A5, A6, A7, A8, Th36;
consider Y being Subset of AS such that
A10:
a = LDir Y
and
A11:
Y is being_line
by Th14;
assume
a <> b
; A = K
then A12:
not Y // Y9
by A10, A11, A5, A6, Th11;
consider X being Subset of AS such that
A13:
A = PDir X
and
A14:
X is being_plane
by Th15;
A15:
Y9 '||' X
by A3, A5, A6, A13, A14, Th36;
A16:
Y '||' X9
by A2, A10, A11, A7, A8, Th36;
Y '||' X
by A1, A10, A11, A13, A14, Th36;
then
X '||' X9
by A11, A6, A14, A8, A12, A16, A15, A9, Th5;
hence
A = K
by A13, A14, A7, A8, Th13; verum