let I be set ; :: thesis: for A being ManySortedSet of holds [0] I c= A
let A be ManySortedSet of ; :: thesis: [0] I c= A
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or ([0] I) . i c= A . i )
assume i in I ; :: thesis: ([0] I) . i c= A . i
([0] I) . i = {} by PBOOLE:5;
hence ([0] I) . i c= A . i by XBOOLE_1:2; :: thesis: verum