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