let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X /\ Y misses X \ Y
let X, Y be ManySortedSet of I; :: thesis: X /\ Y misses X \ Y
( X /\ Y c= Y & X \ Y misses Y ) by Th15, Th108;
hence X /\ Y misses X \ Y by Th107; :: thesis: verum