let I be set ; :: thesis: for x, A, B being ManySortedSet of st ( x in A or x = B ) holds
x in A \/ {B}
let x, A, B be ManySortedSet of ; :: thesis: ( ( x in A or x = B ) implies x in A \/ {B} )
assume A1: ( x in A or x = B ) ; :: thesis: x in A \/ {B}
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or x . i in (A \/ {B}) . i )
assume A2: i in I ; :: thesis: x . i in (A \/ {B}) . i

per cases ( x in A or x = B ) by A1;

suppose x in A ; :: thesis: x . i in (A \/ {B}) . i

then x . i in A . i by A2, PBOOLE:def 4;
then x . i in (A . i) \/ {(B . i)} by SETWISEO:6;
then x . i in (A . i) \/ ({B} . i) by A2, Def1;
hence x . i in (A \/ {B}) . i by A2, PBOOLE:def 7; :: thesis: verum

end;

suppose x = B ; :: thesis: x . i in (A \/ {B}) . i

then x . i in (A . i) \/ {(B . i)} by SETWISEO:6;
then x . i in (A . i) \/ ({B} . i) by A2, Def1;
hence x . i in (A \/ {B}) . i by A2, PBOOLE:def 7; :: thesis: verum

end;

end;