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 13 :: thesis: verum