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