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