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