let I be set ; :: thesis: for X, Y being ManySortedSet of I holds
( (X \ Y) \/ (X /\ Y) = X & (X /\ Y) \/ (X \ Y) = X )
let X, Y be ManySortedSet of I; :: thesis: ( (X \ Y) \/ (X /\ Y) = X & (X /\ Y) \/ (X \ Y) = X )
thus (X \ Y) \/ (X /\ Y) = X \ (Y \ Y) by Th70
.= X \ ([[0]] I) by Th58
.= X by Th65 ; :: thesis: (X /\ Y) \/ (X \ Y) = X
hence (X /\ Y) \/ (X \ Y) = X ; :: thesis: verum