theorem Th8: :: MIDSP_1:8

for M being MidSp
for a, x, x9 being Element of M st x @ a = x9 @ a holds
x = x9