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