let M be MidSp; :: thesis: for a, b being Element of M holds [a,(a @ b)] ## [(a @ b),b]
let a, b be Element of M; :: thesis: [a,(a @ b)] ## [(a @ b),b]
a @ b = (a @ b) @ (a @ b) by Def3;
then a,a @ b @@ a @ b,b ;
hence [a,(a @ b)] ## [(a @ b),b] ; :: thesis: verum