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 Th14, Th15;
hence X /\ Y c= X \/ Z by Th13; :: thesis: verum