let M be MidSp; :: thesis: for r, p being Element of [: the carrier of M, the carrier of M:] holds
( r in p ~ iff r ## p )
let r, p be Element of [: the carrier of M, the carrier of M:]; :: thesis: ( r in p ~ iff r ## p )
thus ( r in p ~ implies r ## p ) :: thesis: ( r ## p implies r in p ~ )

proof

assume r in p ~ ; :: thesis: r ## p
then ex q being Element of [: the carrier of M, the carrier of M:] st
( r = q & q ## p ) ;
hence r ## p ; :: thesis: verum

end;

thus ( r ## p implies r in p ~ ) ; :: thesis: verum