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