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 is_collinear
let x, y be Element of S; :: thesis: ( x <> y implies ex z being Element of S st not x,y,z is_collinear )
assume A1: x <> y ; :: thesis: not for z being Element of S holds x,y,z is_collinear
consider a, b, c being Element of S such that
A2: not a,b,c is_collinear by Th42;
assume A3: for z being Element of S holds x,y,z is_collinear ; :: thesis: contradiction
then A4: x,y,c is_collinear ;
( x,y,a is_collinear & x,y,b is_collinear ) by A3;
hence contradiction by A1, A2, A4, Th38; :: thesis: verum