let AS be AffinSpace; :: thesis: for x, y being Element of st x <> y holds
ex z being Element of st not LIN x,y,z
let x, y be Element of ; :: thesis: ( x <> y implies ex z being Element of st not LIN x,y,z )
assume A1: x <> y ; :: thesis: not for z being Element of holds LIN x,y,z
consider a, b, c being Element of such that
A2: not LIN a,b,c by Th21;
assume A3: for z being Element of holds LIN x,y,z ; :: thesis: contradiction
then A4: LIN x,y,b ;
A5: LIN x,y,c by A3;
LIN x,y,a by A3;
hence contradiction by A1, A2, A4, A5, Th17; :: thesis: verum