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

now

let i be set ; :: thesis: ( i in I implies x . b₁ = y . b₁ )
assume A2: i in I ; :: thesis: x . b₁ = y . b₁

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

suppose A3: {x} \/ {y} = {x} ; :: thesis: x . b₁ = y . b₁

{(x . i)} \/ {(y . i)} = {(x . i)} \/ ({y} . i) by A2, Def1
.= ({x} . i) \/ ({y} . i) by A2, Def1
.= ({x} \/ {y}) . i by A2, PBOOLE:def 7
.= {(x . i)} by A2, A3, Def1 ;
hence x . i = y . i by ZFMISC_1:13; :: thesis: verum

end;

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

{(x . i)} \/ {(y . i)} = {(x . i)} \/ ({y} . i) by A2, Def1
.= ({x} . i) \/ ({y} . i) by A2, Def1
.= ({x} \/ {y}) . i by A2, PBOOLE:def 7
.= {(y . i)} by A2, A4, Def1 ;
hence x . i = y . i by ZFMISC_1:13; :: thesis: verum

end;

end;

end;

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