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

per cases ( {x} /\ {y} = {x} or {x} /\ {y} = {y} ) by A1;

suppose A2: {x} /\ {y} = {x} ; :: thesis: x = y

now

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

end;

hence x = y by PBOOLE:3; :: thesis: verum

end;

suppose A4: {x} /\ {y} = {y} ; :: thesis: x = y

now

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

end;

hence x = y by PBOOLE:3; :: thesis: verum

end;

end;