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 Th43;
hence ([[0]] I) \ X = [[0]] I by Th52; :: thesis: verum