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