theorem :: MIDSP_1:24

for M being MidSp
for p, q, r being Element of [: the carrier of M, the carrier of M:] st p ## q holds
( r ## p iff r ## q ) by Th21;