let AS be AffinSpace; for o, a, b, a', b' being Element of st not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & a' = b' holds
( a' = o & b' = o )
let o, a, b, a', b' be Element of ; ( not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & a' = b' implies ( a' = o & b' = o ) )
assume that
A1:
not LIN o,a,b
and
A2:
LIN o,a,a'
and
A3:
LIN o,b,b'
and
A4:
a' = b'
; ( a' = o & b' = o )
set A = Line o,a;
set C = Line o,b;
A5:
o in Line o,a
by Th26;
A6:
o <> b
by A1, Th16;
then A7:
Line o,b is being_line
by Def3;
A8:
o <> a
by A1, Th16;
then A9:
Line o,a is being_line
by Def3;
A10:
a in Line o,a
by Th26;
then A11:
a' in Line o,a
by A2, A8, A9, A5, Th39;
A12:
b in Line o,b
by Th26;
A13:
o in Line o,b
by Th26;
then A14:
b' in Line o,b
by A3, A6, A7, A12, Th39;
Line o,a <> Line o,b
by A1, A9, A5, A10, A12, Th33;
hence
( a' = o & b' = o )
by A4, A9, A7, A5, A13, A14, A11, Th30; verum