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