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