let I be set ; :: thesis: for X, Y being ManySortedSet of holds X /\ Y misses X \ Y
let X, Y be ManySortedSet of ; :: thesis: X /\ Y misses X \ Y
A1: X /\ Y c= Y by Th17;
X \ Y misses Y by Th118;
hence X /\ Y misses X \ Y by A1, Th116; :: thesis: verum