let I be set ; :: thesis: for x, X being ManySortedSet of I st x in X holds
X /\ {x} = {x}
let x, X be ManySortedSet of I; :: thesis: ( x in X implies X /\ {x} = {x} )
assume A1: x in X ; :: thesis: X /\ {x} = {x}

now

let i be set ; :: thesis: ( i in I implies (X /\ {x}) . i = {x} . i )
assume A2: i in I ; :: thesis: (X /\ {x}) . i = {x} . i
then A3: x . i in X . i by A1, PBOOLE:def 1;
thus (X /\ {x}) . i = (X . i) /\ ({x} . i) by A2, PBOOLE:def 5
.= (X . i) /\ {(x . i)} by A2, Def1
.= {(x . i)} by A3, ZFMISC_1:46
.= {x} . i by A2, Def1 ; :: thesis: verum

end;

hence X /\ {x} = {x} by PBOOLE:3; :: thesis: verum