let I be set ; :: thesis: for X being ManySortedSet of I st X c= [[0]] I holds
X = [[0]] I
let X be ManySortedSet of I; :: thesis: ( X c= [[0]] I implies X = [[0]] I )
assume X c= [[0]] I ; :: thesis: X = [[0]] I
hence ( X c= [[0]] I & [[0]] I c= X ) by Th49; :: according to PBOOLE:def 10 :: thesis: verum