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) \/ (X \ Y) by Th69
.= ([[0]] I) \/ (X \ Y) by Th52
.= X \ Y by Th22, Th43 ; :: thesis: verum