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