:: deftheorem defines ID MIDSP_1:def 8 :
for M being MidSp holds ID M = { p where p is Element of [: the carrier of M, the carrier of M:] : p `1 = p `2 } ;