let M be MidSp; :: thesis: for p, q being Element of [: the carrier of M, the carrier of M:] st p ~ = q ~ holds
p ## q
let p, q be Element of [: the carrier of M, the carrier of M:]; :: thesis: ( p ~ = q ~ implies p ## q )
p in p ~ ;
hence ( p ~ = q ~ implies p ## q ) by Th26; :: thesis: verum