let S be OAffinSpace; for x, y being Element of S ex z being Element of S st
( Mid x,y,z & y <> z )
let x, y be Element of S; ex z being Element of S st
( Mid x,y,z & y <> z )
consider z being Element of S such that
A1:
x,y // y,z
and
x,y // y,z
and
A2:
y <> z
by ANALOAF:def 5;
Mid x,y,z
by A1;
hence
ex z being Element of S st
( Mid x,y,z & y <> z )
by A2; verum