theorem Th21: :: MIDSP_1:21

for M being MidSp
for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q & p ## r holds
q ## r by Th17;