let S be OAffinSpace; :: thesis: for x, y, z being Element of S st Mid x,y,z & Mid y,x,z holds
x = y
let x, y, z be Element of S; :: thesis: ( Mid x,y,z & Mid y,x,z implies x = y )
assume A1: ( Mid x,y,z & Mid y,x,z ) ; :: thesis: x = y
then ( x,y // y,z & y,x // x,z ) by Def3;
then A2: ( x,y // x,z & x,y // z,x ) by ANALOAF:def 5;
( x = z implies x = y ) by A1, Th12;
hence x = y by A2, Th8; :: thesis: verum