let I be set ; :: thesis: for x, y being ManySortedSet of holds
( {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y} )
let x, y be ManySortedSet of ; :: thesis: ( {x} /\ {x,y} = {x} & {y} /\ {x,y} = {y} )
thus {x} /\ {x,y} = {x} :: thesis: {y} /\ {x,y} = {y}

proof

now

let i be set ; :: thesis: ( i in I implies ({x} /\ {x,y}) . i = {x} . i )
assume A1: i in I ; :: thesis: ({x} /\ {x,y}) . i = {x} . i
hence ({x} /\ {x,y}) . i = ({x} . i) /\ ({x,y} . i) by PBOOLE:def 8
.= {(x . i)} /\ ({x,y} . i) by A1, Def1
.= {(x . i)} /\ {(x . i),(y . i)} by A1, Def2
.= {(x . i)} by ZFMISC_1:19
.= {x} . i by A1, Def1 ;
:: thesis: verum

end;

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

end;

thus {y} /\ {x,y} = {y} :: thesis: verum

proof

now

let i be set ; :: thesis: ( i in I implies ({y} /\ {x,y}) . i = {y} . i )
assume A2: i in I ; :: thesis: ({y} /\ {x,y}) . i = {y} . i
hence ({y} /\ {x,y}) . i = ({y} . i) /\ ({x,y} . i) by PBOOLE:def 8
.= {(y . i)} /\ ({x,y} . i) by A2, Def1
.= {(y . i)} /\ {(x . i),(y . i)} by A2, Def2
.= {(y . i)} by ZFMISC_1:19
.= {y} . i by A2, Def1 ;
:: thesis: verum

end;

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

end;