let I, J be set ; :: thesis: for A being ManySortedSet of I
for B being ManySortedSet of J st A cc= B & B cc= A holds
A = B
let A be ManySortedSet of I; :: thesis: for B being ManySortedSet of J st A cc= B & B cc= A holds
A = B
let B be ManySortedSet of J; :: thesis: ( A cc= B & B cc= A implies A = B )
assume that
A1: A cc= B and
A2: B cc= A ; :: thesis: A = B
A3: I c= J by A1, Def2;
J c= I by A2, Def2;
then I = J by A3, XBOOLE_0:def 10;
then reconsider B9 = B as ManySortedSet of I ;

now

let i be set ; :: thesis: ( i in I implies A . i = B9 . i )
assume i in I ; :: thesis: A . i = B9 . i
then ( A . i c= B . i & B . i c= A . i ) by A1, A2, A3, Def2;
hence A . i = B9 . i by XBOOLE_0:def 10; :: thesis: verum

end;

hence A = B by PBOOLE:3; :: thesis: verum