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