let b be bag of X; :: thesis: ( b is univariate implies not b is empty-yielding )
assume b is univariate ; :: thesis: b is empty-yielding
then consider x being Element of X such that
A1: support b = {x} ;
x in support b by A1, TARSKI:def 1;
then b . x <> 0 by PRE_POLY:def 7;
then b . x <> (EmptyBag X) . x by PBOOLE:5;
hence b is empty-yielding by PRE_POLY:def 18; :: thesis: verum