let I be set ; :: thesis: for X being ManySortedSet of I holds EmptyMS I c= X
let X be ManySortedSet of I; :: thesis: EmptyMS I c= X
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies (EmptyMS I) . i c= X . i )
assume i in I ; :: thesis: (EmptyMS I) . i c= X . i
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (EmptyMS I) . i or e in X . i )
assume e in (EmptyMS I) . i ; :: thesis: e in X . i
hence e in X . i ; :: thesis: verum