let I be set ; :: thesis: for x, A, B being ManySortedSet of I st ( x in A or x = B ) holds
x in A (\/) {B}
let x, A, B be ManySortedSet of I; :: 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 object ; :: according to PBOOLE:def 1 :: 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;
then x . i in (A . i) \/ {(B . i)} by ZFMISC_1:136;
then x . i in (A . i) \/ ({B} . i) by A2, Def1;
hence x . i in (A (\/) {B}) . i by A2, PBOOLE:def 4; :: thesis: verum

end;

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

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

end;

end;