let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds X /\ Y c= X \/ Z
let X, Y, Z be ManySortedSet of I; :: thesis: X /\ Y c= X \/ Z
( X /\ Y c= X & X c= X \/ Z ) by Th16, Th17;
hence X /\ Y c= X \/ Z by Th15; :: thesis: verum