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