let I be set ; :: thesis: for X, Y being ManySortedSet of I st ( X c= [|X,Y|] or X c= [|Y,X|] ) holds
X = EmptyMS I
let X, Y be ManySortedSet of I; :: thesis: ( ( X c= [|X,Y|] or X c= [|Y,X|] ) implies X = EmptyMS I )
assume A1: ( X c= [|X,Y|] or X c= [|Y,X|] ) ; :: thesis: X = EmptyMS I

per cases ( X c= [|X,Y|] or X c= [|Y,X|] ) by A1;

suppose A2: X c= [|X,Y|] ; :: thesis: X = EmptyMS I

now :: thesis: for i being object st i in I holds
X . i = (EmptyMS I) . i

let i be object ; :: thesis: ( i in I implies X . i = (EmptyMS I) . i )
assume A3: i in I ; :: thesis: X . i = (EmptyMS I) . i
then X . i c= [|X,Y|] . i by A2;
then X . i c= [:(X . i),(Y . i):] by A3, PBOOLE:def 16;
hence X . i = {} by ZFMISC_1:111
.= (EmptyMS I) . i by PBOOLE:5 ;
:: thesis: verum

end;

hence X = EmptyMS I ; :: thesis: verum

end;

suppose A4: X c= [|Y,X|] ; :: thesis: X = EmptyMS I

now :: thesis: for i being object st i in I holds
X . i = (EmptyMS I) . i

let i be object ; :: thesis: ( i in I implies X . i = (EmptyMS I) . i )
assume A5: i in I ; :: thesis: X . i = (EmptyMS I) . i
then X . i c= [|Y,X|] . i by A4;
then X . i c= [:(Y . i),(X . i):] by A5, PBOOLE:def 16;
hence X . i = {} by ZFMISC_1:111
.= (EmptyMS I) . i by PBOOLE:5 ;
:: thesis: verum

end;

hence X = EmptyMS I ; :: thesis: verum

end;

end;