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