let I be non empty set ; :: thesis: for X being ManySortedSet of I holds not X overlaps [[0]] I
let X be ManySortedSet of I; :: thesis: not X overlaps [[0]] I
assume X overlaps [[0]] I ; :: thesis: contradiction
then ex x being ManySortedSet of I st
( x in X & x in [[0]] I ) by Th11;
hence contradiction by Th136; :: thesis: verum