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