let AS be AffinSpace; 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; ( x <> y implies ex z being Element of AS st not LIN x,y,z )
assume A1:
x <> y
; 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
; 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; verum