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