:: deftheorem defines ## MIDSP_1:def 5 :
for M being MidSp
for p, q being Element of [: the carrier of M, the carrier of M:] holds
( p ## q iff p `1 ,p `2 @@ q `1 ,q `2 );