let M be MidSp; :: thesis: for a, b being Element of holds [a,(a @ b)] ## [(a @ b),b]
let a, b be Element of ; :: 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