let AS be AffinSpace; :: thesis: for o, a, b, a', b', x being Element of st not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & LIN o,b,x & a,b // a',b' & a,b // a',x holds
b' = x
let o, a, b, a', b', x be Element of ; :: thesis: ( not LIN o,a,b & LIN o,a,a' & LIN o,b,b' & LIN o,b,x & a,b // a',b' & a,b // a',x implies b' = x )
assume that
A1: not LIN o,a,b and
A2: LIN o,a,a' and
A3: LIN o,b,b' and
A4: LIN o,b,x and
A5: a,b // a',b' and
A6: a,b // a',x ; :: thesis: b' = x
set A = Line o,a;
set C = Line o,b;
set P = Line a',b';
A7: a' in Line a',b' by Th26;
assume A8: b' <> x ; :: thesis: contradiction
A9: a' <> b'

proof

assume A10: a' = b' ; :: thesis: contradiction
then a' = o by A1, A2, A3, Th68;
hence contradiction by A1, A4, A6, A8, A10, Th69; :: thesis: verum

end;

then A11: Line a',b' is being_line by Def3;
A12: o <> b by A1, Th16;
then A13: Line o,b is being_line by Def3;
A14: b' in Line a',b' by Th26;
a <> b by A1, Th16;
then a',b' // a',x by A5, A6, Th14;
then LIN a',b',x by Def1;
then A15: x in Line a',b' by A9, A11, A7, A14, Th39;
A16: b in Line o,b by Th26;
A17: o in Line o,b by Th26;
then A18: x in Line o,b by A4, A12, A13, A16, Th39;
b' in Line o,b by A3, A12, A13, A17, A16, Th39;
then A19: a' in Line o,b by A8, A13, A11, A7, A14, A18, A15, Th30;
A20: o <> a by A1, Th16;
then A21: Line o,a is being_line by Def3;
A22: a' <> o

proof

assume A23: a' = o ; :: thesis: contradiction
then b' = o by A1, A3, A5, Th69;
hence contradiction by A1, A4, A6, A8, A23, Th69; :: thesis: verum

end;

A24: o in Line o,a by Th26;
A25: a in Line o,a by Th26;
then a' in Line o,a by A2, A20, A21, A24, Th39;
then b in Line o,a by A22, A21, A13, A24, A17, A16, A19, Th30;
hence contradiction by A1, A21, A24, A25, Th33; :: thesis: verum