let S be OAffinSpace; :: thesis: 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; :: thesis: 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; :: thesis: verum