let AS be AffinSpace; :: thesis: for x, y being Element of AS st x <> y holds
ex z being Element of AS st not LIN x,y,z
let x, y be Element of AS; :: thesis: ( x <> y implies ex z being Element of AS st not LIN x,y,z )
assume A1: x <> y ; :: thesis: not for z being Element of AS holds LIN x,y,z
consider a, b, c being Element of AS such that
A2: not LIN a,b,c by Th11;
assume A3: for z being Element of AS 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, Th7; :: thesis: verum