let I be set ; :: thesis: for x1, x2, A being ManySortedSet of I st ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) holds
A c= {x1,x2}
let x1, x2, A be ManySortedSet of I; :: thesis: ( ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) implies A c= {x1,x2} )
assume A1: ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) ; :: thesis: A c= {x1,x2}
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or A . i c= {x1,x2} . i )
assume A2: i in I ; :: thesis: A . i c= {x1,x2} . i

per cases ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) by A1;

suppose A = EmptyMS I ; :: thesis: A . i c= {x1,x2} . i

then A . i = {} by PBOOLE:5;
then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:36;
hence A . i c= {x1,x2} . i by A2, Def2; :: thesis: verum

end;

suppose A = {x1} ; :: thesis: A . i c= {x1,x2} . i

then A . i = {(x1 . i)} by A2, Def1;
then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:36;
hence A . i c= {x1,x2} . i by A2, Def2; :: thesis: verum

end;

suppose A = {x2} ; :: thesis: A . i c= {x1,x2} . i

then A . i = {(x2 . i)} by A2, Def1;
then A . i c= {(x1 . i),(x2 . i)} by ZFMISC_1:36;
hence A . i c= {x1,x2} . i by A2, Def2; :: thesis: verum

end;

suppose A = {x1,x2} ; :: thesis: A . i c= {x1,x2} . i

hence A . i c= {x1,x2} . i ; :: thesis: verum

end;

end;