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

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