theorem Th13: :: MIDSP_1:13

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