theorem Th41: :: MIDSP_1:41
for M being MidSp
for a, b being Element of M holds [a,(a @ b)] ## [(a @ b),b]