theorem Th20: :: MIDSP_1:20

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