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