theorem Th16: :: MIDSP_1:16

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