let I be set ; :: thesis: for x, y, X being ManySortedSet of I st y in X (\) {x} holds
y in X
let x, y, 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 object ; :: according to PBOOLE:def 1 :: 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;
then y . i in (X . i) \ ({x} . i) by A2, PBOOLE:def 6;
then y . i in (X . i) \ {(x . i)} by A2, Def1;
hence y . i in X . i by ZFMISC_1:56; :: thesis: verum