let AS be AffinSpace; :: thesis: for o, a, b, b9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds
b = b9
let o, a, b, b9 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, Def1;
then A4: LIN b,b9,a by Th15;
A5: LIN b,b9,b by Th16;
assume A6: b <> b9 ; :: thesis: contradiction
LIN b,b9,o by A2, Th15;
hence contradiction by A1, A6, A4, A5, Th17; :: thesis: verum