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 that
A1: Mid x,y,z and
A2: Mid y,x,z ; :: thesis: x = y
x,y // y,z by A1;
then A3: x,y // x,z by ANALOAF:def 5;
y,x // x,z by A2;
then A4: x,y // z,x by ANALOAF:def 5;
( x = z implies x = y ) by A1, Th8;
hence x = y by A3, A4, Th5; :: thesis: verum