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