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 ~ )
proof
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 ~ )
proof
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;
thus ( x in q ~ implies x in p ~ ) :: thesis: verum
proof
assume A3: x in q ~ ; :: thesis: x in p ~
then reconsider r = x as Element of [: the carrier of M, the carrier of M:] ;
r ## q by A3, Th26;
then r ## p by A1, Th21;
hence x in p ~ ; :: thesis: verum
end;
end;
hence p ~ = q ~ by TARSKI:2; :: thesis: verum