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

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