theorem Th5: :: MIDSP_1:5

for M being MidSp
for a, b, c being Element of M holds (a @ b) @ c = (a @ c) @ (b @ c)