let I be set ; :: thesis: for X, Y being ManySortedSet of I holds (X \ Y) /\ Y = [[0]] I
let X, Y be ManySortedSet of I; :: thesis: (X \ Y) /\ Y = [[0]] I
A1: Y /\ X c= Y by Th15;
thus (X \ Y) /\ Y = (Y /\ X) \ Y by Th62
.= [[0]] I by A1, Th52 ; :: thesis: verum
thus verum ; :: thesis: verum