let M be MidSp; :: thesis: for a, b being Element of M st a @ b = a holds
a = b
let a, b be Element of M; :: thesis: ( a @ b = a implies a = b )
assume A1: a @ b = a ; :: thesis: a = b
consider x being Element of M such that
A2: x @ a = b by Def3;
b = (x @ a) @ b by A2, Def3
.= (x @ b) @ a by A1, Th5
.= a by A1, A2, Th5 ;
hence a = b ; :: thesis: verum