let I be set ; :: thesis: for x, X being ManySortedSet of I st not I is empty & X (\) {x} = X holds
not x in X
let x, X be ManySortedSet of I; :: thesis: ( not I is empty & X (\) {x} = X implies not x in X )
assume that
A1: not I is empty and
A2: X (\) {x} = X and
A3: x in X ; :: thesis: contradiction

A4: now :: thesis: for i being object st i in I holds
(X . i) \ {(x . i)} = X . i

let i be object ; :: thesis: ( i in I implies (X . i) \ {(x . i)} = X . i )
assume A5: i in I ; :: thesis: (X . i) \ {(x . i)} = X . i
hence (X . i) \ {(x . i)} = (X . i) \ ({x} . i) by Def1
.= X . i by A2, A5, PBOOLE:def 6 ;
:: thesis: verum

end;

now :: thesis: ex i being object st
( i in I & not x . i in X . i )

consider i being object such that
A6: i in I by A1, XBOOLE_0:def 1;
take i = i; :: thesis: ( i in I & not x . i in X . i )
thus i in I by A6; :: thesis: not x . i in X . i
(X . i) \ {(x . i)} = X . i by A4, A6;
hence not x . i in X . i by ZFMISC_1:57; :: thesis: verum

end;

hence contradiction by A3; :: thesis: verum