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 Th70
.= ([[0]] I) \/ (X /\ Y) by Th58
.= X /\ Y by Th53 ; :: thesis: verum