let AS be AffinSpace; for a, a9, b, b9, o being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 holds
( a9 = o & b9 = o )
let a, a9, b, b9, o be Element of AS; ( not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 implies ( a9 = o & b9 = o ) )
assume that
A1:
not LIN o,a,b
and
A2:
LIN o,a,a9
and
A3:
LIN o,b,b9
and
A4:
a9 = b9
; ( a9 = o & b9 = o )
set A = Line (o,a);
set C = Line (o,b);
A5:
o in Line (o,a)
by Th14;
A6:
o <> b
by A1, Th6;
then A7:
Line (o,b) is being_line
;
A8:
o <> a
by A1, Th6;
then A9:
Line (o,a) is being_line
;
A10:
a in Line (o,a)
by Th14;
then A11:
a9 in Line (o,a)
by A2, A8, A9, A5, Th24;
A12:
b in Line (o,b)
by Th14;
A13:
o in Line (o,b)
by Th14;
then A14:
b9 in Line (o,b)
by A3, A6, A7, A12, Th24;
Line (o,a) <> Line (o,b)
by A1, A9, A5, A10, A12, Th20;
hence
( a9 = o & b9 = o )
by A4, A9, A7, A5, A13, A14, A11, Th17; verum