let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X /\ (X /\ Y) = X /\ Y
let X, Y be ManySortedSet of I; :: thesis: X /\ (X /\ Y) = X /\ Y
thus X /\ (X /\ Y) = (X /\ X) /\ Y by Th29
.= X /\ Y ; :: thesis: verum