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