let AS be AffinSpace; :: thesis: for a, a9, b, b9, o being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9 = o holds
b9 = o
let a, a9, b, b9, o 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 :: thesis: not a,b // a9,b

assume a,b // a9,b ; :: thesis: contradiction
then b,a // b,a9 by Th3;
then LIN b,a,a9 ;
hence contradiction by A1, A4, Th5; :: thesis: verum

end;

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