let AS be AffinSpace; :: thesis: for o, a, b, b', a' being Element of st not LIN o,a,b & LIN o,b,b' & a,b // a',b' & a' = o holds
b' = o
let o, a, b, b', a' be Element of ; :: thesis: ( not LIN o,a,b & LIN o,b,b' & a,b // a',b' & a' = o implies b' = o )
assume that
A1: not LIN o,a,b and
A2: LIN o,b,b' and
A3: a,b // a',b' and
A4: a' = o ; :: thesis: b' = o

A5: now

assume a,b // a',b ; :: thesis: contradiction
then b,a // b,a' by Th13;
then LIN b,a,a' by Def1;
hence contradiction by A1, A4, Th15; :: thesis: verum

end;

a',b // a',b' by A2, A4, Def1;
hence b' = o by A3, A4, A5, Th14; :: thesis: verum