let I, J be set ; :: thesis: for A being ManySortedSet of
for B being ManySortedSet of st A cc= B & B cc= A holds
A = B
let A be ManySortedSet of ; :: thesis: for B being ManySortedSet of st A cc= B & B cc= A holds
A = B
let B be ManySortedSet of ; :: 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 & J c= I ) by A1, A2, Def2;
then I = J by XBOOLE_0:def 10;
then reconsider B' = B as ManySortedSet of ;

now

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

end;

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