let I be set ; :: thesis: for X, Y being ManySortedSet of st X c= Y holds
X [= Y
let X, Y be ManySortedSet of ; :: thesis: ( X c= Y implies X [= Y )
assume A1: X c= Y ; :: thesis: X [= Y
let x be ManySortedSet of ; :: according to PBOOLE:def 14 :: thesis: ( x in X implies x in Y )
assume A2: x in X ; :: thesis: x in Y
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( i in I implies x . i in Y . i )
assume i in I ; :: thesis: x . i in Y . i
then ( x . i in X . i & X . i c= Y . i ) by A1, A2, Def4, Def5;
hence x . i in Y . i ; :: thesis: verum