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