theorem Th28: :: MIDSP_1:28

for M being MidSp
for p, q being Element of [: the carrier of M, the carrier of M:] st p ~ = q ~ holds
p ## q