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