let I be set ; :: thesis: for X being ManySortedSet of holds ([0] I) \ X = [0] I
let X be ManySortedSet of ; :: thesis: ([0] I) \ X = [0] I
[0] I c= X by Th49;
hence ([0] I) \ X = [0] I by Th58; :: thesis: verum