let I be non empty set ; :: thesis: for X being ManySortedSet of I st X overlaps X holds
X <> [[0]] I
let X be ManySortedSet of I; :: thesis: ( X overlaps X implies X <> [[0]] I )
X = X /\ X ;
hence ( X overlaps X implies X <> [[0]] I ) by Th139; :: thesis: verum