theorem Th19: :: MIDSP_1:19

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