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