let I be set ; :: thesis: for X, Y being ManySortedSet of I holds (X \ Y) \/ (X /\ Y) = X
let X, Y be ManySortedSet of I; :: thesis: (X \ Y) \/ (X /\ Y) = X
thus (X \ Y) \/ (X /\ Y) = X \ (Y \ Y) by Th64
.= X \ ([[0]] I) by Th52
.= X by Th59 ; :: thesis: verum