theorem :: MIDSP_1:10

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