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 /\ Y c= X by Th15;
then A1: X \/ (X /\ Y) c= X by Th16;
X c= X \/ (X /\ Y) by Th14;
hence X \/ (X /\ Y) = X by A1, Lm1; :: thesis: verum