let M be MidSp; :: thesis: for a, b, c being Element of M st a,a @@ b,c holds
b = c
let a, b, c be Element of M; :: thesis: ( a,a @@ b,c implies b = c )
assume a,a @@ b,c ; :: thesis: b = c
then a @ c = a @ b by Def5;
hence b = c by Th18; :: thesis: verum