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 ~ )

( 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

thus
( r ## p implies r in p ~ )
; :: thesis: verum
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;then ex q being Element of [: the carrier of M, the carrier of M:] st

( r = q & q ## p ) ;

hence r ## p ; :: thesis: verum