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