let S be OAffinSpace; :: thesis: for a, b being Element of S st Mid a,b,a holds
a = b
let a, b be Element of S; :: thesis: ( Mid a,b,a implies a = b )
assume Mid a,b,a ; :: thesis: a = b
then a,b // b,a by Def3;
hence a = b by ANALOAF:def 5; :: thesis: verum