let AS be AffinSpace; :: thesis: for a, b, b9, o being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds
b = b9
let a, b, b9, o be Element of AS; :: thesis: ( not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 implies b = b9 )
assume that
A1: not LIN o,a,b and
A2: LIN o,b,b9 and
A3: a,b // a,b9 ; :: thesis: b = b9
LIN a,b,b9 by A3;
then A4: LIN b,b9,a by Th5;
A5: LIN b,b9,b by Th6;
assume A6: b <> b9 ; :: thesis: contradiction
LIN b,b9,o by A2, Th5;
hence contradiction by A1, A6, A4, A5, Th7; :: thesis: verum