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 :: thesis: for i being object st i in I holds
(X (/\) {x}) . i = {x} . i

let i be object ; :: 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;
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} ; :: thesis: verum