let I be set ; :: thesis: for X, Y being ManySortedSet of I st X c= Y & Y c= X holds
X = Y
let X, Y be ManySortedSet of I; :: thesis: ( X c= Y & Y c= X implies X = Y )
assume A1: ( X c= Y & Y c= X ) ; :: thesis: X = Y

now :: thesis: for i being set st i in I holds
X . i = Y . i

let i be set ; :: thesis: ( i in I implies X . i = Y . i )
assume i in I ; :: thesis: X . i = Y . i
then ( X . i c= Y . i & Y . i c= X . i ) by A1, Def2;
hence X . i = Y . i by XBOOLE_0:def 10; :: thesis: verum

end;

hence X = Y by Th3; :: thesis: verum