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