let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X /\ (X \/ Y) = X
let X, Y be ManySortedSet of I; :: thesis: X /\ (X \/ Y) = X
X c= X \/ Y by Th14;
then A1: X c= X /\ (X \/ Y) by Th17;
X /\ (X \/ Y) c= X by Th15;
hence X /\ (X \/ Y) = X by A1, Lm1; :: thesis: verum