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