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