theorem Th29: :: MIDSP_1:29

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