theorem :: MIDSP_1:14

for M being MidSp
for a, b being Element of M holds a,b @@ a,b ;