let M be MidSp; :: thesis: for a, b being Element of M holds a,b @@ a,b
let a, b be Element of M; :: thesis: a,b @@ a,b
thus a @ b = b @ a ; :: according to MIDSP_1:def 4 :: thesis: verum