let I be set ; :: thesis: for y, X, x being ManySortedSet of I st y in X \ {x} holds
y in X
let y, X, x be ManySortedSet of I; :: thesis: ( y in X \ {x} implies y in X )
assume A1: y in X \ {x} ; :: thesis: y in X
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or y . i in X . i )
assume A2: i in I ; :: thesis: y . i in X . i
then y . i in (X \ {x}) . i by A1, PBOOLE:def 4;
then y . i in (X . i) \ ({x} . i) by A2, PBOOLE:def 9;
then y . i in (X . i) \ {(x . i)} by A2, Def1;
hence y . i in X . i by ZFMISC_1:64; :: thesis: verum