let I be set ; :: thesis: for X being ManySortedSet of I holds X \+\ ([[0]] I) = X
let X be ManySortedSet of I; :: thesis: X \+\ ([[0]] I) = X
thus X \+\ ([[0]] I) = X \/ (([[0]] I) \ X) by Th59
.= X \/ ([[0]] I) by Th60
.= X by Th22, Th43 ; :: thesis: verum