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 Def4;
then a,a @ b @@ a @ b,b by Def5;
hence [a,(a @ b)] ## [(a @ b),b] by Th31; :: thesis: verum