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