let AS be AffinSpace; :: thesis: for o, a, b, a9, b9 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 o, a, b, a9, b9 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 Th15;
A6: o <> b by A1, Th7;
then A7: Line (o,b) is being_line by Def3;
A8: o <> a by A1, Th7;
then A9: Line (o,a) is being_line by Def3;
A10: a in Line (o,a) by Th15;
then A11: a9 in Line (o,a) by A2, A8, A9, A5, Th25;
A12: b in Line (o,b) by Th15;
A13: o in Line (o,b) by Th15;
then A14: b9 in Line (o,b) by A3, A6, A7, A12, Th25;
Line (o,a) <> Line (o,b) by A1, A9, A5, A10, A12, Th21;
hence ( a9 = o & b9 = o ) by A4, A9, A7, A5, A13, A14, A11, Th18; :: thesis: verum