let I be set ; :: thesis: for X, Y being ManySortedSet of I st X \/ Y = [0] I holds
( X = [0] I & Y = [0] I )
let X, Y be ManySortedSet of I; :: thesis: ( X \/ Y = [0] I implies ( X = [0] I & Y = [0] I ) )
assume X \/ Y = [0] I ; :: thesis: ( X = [0] I & Y = [0] I )
then ( X c= [0] I & Y c= [0] I ) by Th16;
hence ( X = [0] I & Y = [0] I ) by Th50; :: thesis: verum