let S be OAffinSpace; :: thesis: for x, y being Element of S st x <> y holds
ex z being Element of S st not x,y,z are_collinear
let x, y be Element of S; :: thesis: ( x <> y implies ex z being Element of S st not x,y,z are_collinear )
assume A1: x <> y ; :: thesis: not for z being Element of S holds x,y,z are_collinear
consider a, b, c being Element of S such that
A2: not a,b,c are_collinear by Th36;
assume A3: for z being Element of S holds x,y,z are_collinear ; :: thesis: contradiction
then A4: x,y,c are_collinear ;
( x,y,a are_collinear & x,y,b are_collinear ) by A3;
hence contradiction by A1, A2, A4, Th32; :: thesis: verum