let I be non empty set ; :: thesis: for B being non-empty ManySortedSet of I holds not union (rng B) is empty
let B be non-empty ManySortedSet of I; :: thesis: not union (rng B) is empty
set i = the Element of I;
the Element of I in I ;
then the Element of I in dom B by PARTFUN1:def 2;
then B . the Element of I in rng B by FUNCT_1:def 3;
hence not union (rng B) is empty by ORDERS_1:6; :: thesis: verum