let I be set ; :: thesis: for X, Y being ManySortedSet of I holds (X \ Y) \ Y = X \ Y
let X, Y be ManySortedSet of I; :: thesis: (X \ Y) \ Y = X \ Y
thus (X \ Y) \ Y = X \ (Y \/ Y) by Th79
.= X \ Y ; :: thesis: verum