let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X \/ Y c= Z holds
( X c= Z & Y c= Z )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X \/ Y c= Z implies ( X c= Z & Y c= Z ) )
assume A1: X \/ Y c= Z ; :: thesis: ( X c= Z & Y c= Z )
( X c= X \/ Y & Y c= X \/ Y ) by Th16;
hence ( X c= Z & Y c= Z ) by A1, Th15; :: thesis: verum