theorem Th12: :: MIDSP_1:12

for M being MidSp
for a, b, c being Element of M st a,a @@ b,c holds
b = c by Th8;