theorem Th11: :: MIDSP_1:11

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