let M be MidSp; :: thesis: for a, b, c being Element of M holds a @ (b @ c) = (a @ b) @ (a @ c)
let a, b, c be Element of M; :: thesis: a @ (b @ c) = (a @ b) @ (a @ c)
a @ (b @ c) = (a @ a) @ (b @ c) by Def3
.= (a @ b) @ (a @ c) by Def3 ;
hence a @ (b @ c) = (a @ b) @ (a @ c) ; :: thesis: verum