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

assume A1: p ## q ; :: thesis: p ~ = q ~

for x being object holds

( x in p ~ iff x in q ~ )

p ~ = q ~

let p, q be Element of [: the carrier of M, the carrier of M:]; :: thesis: ( p ## q implies p ~ = q ~ )

assume A1: p ## q ; :: thesis: p ~ = q ~

for x being object holds

( x in p ~ iff x in q ~ )

proof

hence
p ~ = q ~
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in p ~ iff x in q ~ )

thus ( x in p ~ implies x in q ~ ) :: thesis: ( x in q ~ implies x in p ~ )

end;thus ( x in p ~ implies x in q ~ ) :: thesis: ( x in q ~ implies x in p ~ )

proof

thus
( x in q ~ implies x in p ~ )
:: thesis: verum
assume A2:
x in p ~
; :: thesis: x in q ~

then reconsider r = x as Element of [: the carrier of M, the carrier of M:] ;

r ## p by A2, Th26;

then r ## q by A1, Th21;

hence x in q ~ ; :: thesis: verum

end;then reconsider r = x as Element of [: the carrier of M, the carrier of M:] ;

r ## p by A2, Th26;

then r ## q by A1, Th21;

hence x in q ~ ; :: thesis: verum