:: deftheorem defines ~ MIDSP_1:def 6 :
for M being MidSp
for p being Element of [: the carrier of M, the carrier of M:] holds p ~ = { q where q is Element of [: the carrier of M, the carrier of M:] : q ## p } ;