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

A5: now

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

end;

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