let I be set ; :: thesis: for X, Y being ManySortedSet of I st X c= Y holds
X [= Y
let X, Y be ManySortedSet of I; :: thesis: ( X c= Y implies X [= Y )
assume A1: X c= Y ; :: thesis: X [= Y
let x be ManySortedSet of I; :: according to PBOOLE:def 11 :: thesis: ( x in X implies x in Y )
assume A2: x in X ; :: thesis: x in Y
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( i in I implies x . i in Y . i )
assume A3: i in I ; :: thesis: x . i in Y . i
then A4: X . i c= Y . i by A1;
x . i in X . i by A2, A3;
hence x . i in Y . i by A4; :: thesis: verum