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