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