let I be set ; :: thesis: for x, y, X being ManySortedSet of I st not I is empty & {x,y} \ X = {x,y} holds
( not x in X & not y in X )
let x, y, X be ManySortedSet of I; :: thesis: ( not I is empty & {x,y} \ X = {x,y} implies ( not x in X & not y in X ) )
assume not I is empty ; :: thesis: ( not {x,y} \ X = {x,y} or ( not x in X & not y in X ) )
then consider i being set such that
A1: i in I by XBOOLE_0:def 1;
thus ( {x,y} \ X = {x,y} implies ( not x in X & not y in X ) ) :: thesis: verum

proof

assume A2: {x,y} \ X = {x,y} ; :: thesis: ( not x in X & not y in X )
thus not x in X :: thesis: not y in X

proof

assume A3: x in X ; :: thesis: contradiction
{(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by A1, Def2
.= ({x,y} \ X) . i by A1, PBOOLE:def 9
.= {(x . i),(y . i)} by A1, A2, Def2 ;
then not x . i in X . i by ZFMISC_1:72;
hence contradiction by A1, A3, PBOOLE:def 4; :: thesis: verum

end;

assume A4: y in X ; :: thesis: contradiction
{(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by A1, Def2
.= ({x,y} \ X) . i by A1, PBOOLE:def 9
.= {(x . i),(y . i)} by A1, A2, Def2 ;
then not y . i in X . i by ZFMISC_1:72;
hence contradiction by A1, A4, PBOOLE:def 4; :: thesis: verum

end;