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 Th38;
hence X c= Y \/ Z by Th17; :: thesis: verum