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 Th41; :: thesis: verum