let I be set ; :: thesis: for A, B, X, Y being ManySortedSet of st A is non-empty & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) holds
B c= Y
let A, B, X, Y be ManySortedSet of ; :: thesis: ( A is non-empty & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) implies B c= Y )
assume that
A1: A is non-empty and
A2: ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) ; :: thesis: B c= Y

per cases ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) by A2;

suppose A3: [|A,B|] c= [|X,Y|] ; :: thesis: B c= Y

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or B . i c= Y . i )
assume A4: i in I ; :: thesis: B . i c= Y . i
then [|A,B|] . i c= [|X,Y|] . i by A3, PBOOLE:def 5;
then [:(A . i),(B . i):] c= [|X,Y|] . i by A4, PBOOLE:def 21;
then A5: [:(A . i),(B . i):] c= [:(X . i),(Y . i):] by A4, PBOOLE:def 21;
not A . i is empty by A1, A4, PBOOLE:def 16;
hence B . i c= Y . i by A5, ZFMISC_1:139; :: thesis: verum

end;

suppose A6: [|B,A|] c= [|Y,X|] ; :: thesis: B c= Y

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or B . i c= Y . i )
assume A7: i in I ; :: thesis: B . i c= Y . i
then [|B,A|] . i c= [|Y,X|] . i by A6, PBOOLE:def 5;
then [:(B . i),(A . i):] c= [|Y,X|] . i by A7, PBOOLE:def 21;
then A8: [:(B . i),(A . i):] c= [:(Y . i),(X . i):] by A7, PBOOLE:def 21;
not A . i is empty by A1, A7, PBOOLE:def 16;
hence B . i c= Y . i by A8, ZFMISC_1:139; :: thesis: verum

end;

end;