let M be MidSp; :: thesis: for a, b, c, d being Element of M st a,b @@ c,d holds
c,d @@ a,b
let a, b, c, d be Element of M; :: thesis: ( a,b @@ c,d implies c,d @@ a,b )
assume a @ d = b @ c ; :: according to MIDSP_1:def 4 :: thesis: c,d @@ a,b
hence c @ b = d @ a ; :: according to MIDSP_1:def 4 :: thesis: verum