let S be OAffinSpace; :: thesis: for x, y being Element of ex z being Element of st
( Mid x,y,z & y <> z )
let x, y be Element of ; :: thesis: ex z being Element of st
( Mid x,y,z & y <> z )
consider z being Element of 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, Def3;
hence ex z being Element of st
( Mid x,y,z & y <> z ) by A2; :: thesis: verum