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