:: deftheorem defines @@ MIDSP_1:def 4 :
for M being MidSp
for a, b, c, d being Element of M holds
( a,b @@ c,d iff a @ d = b @ c );