let b be bag of X; :: thesis: ( b is univariate implies not b is empty )
assume b is univariate ; :: thesis: not b is empty
then consider x being Element of X such that
A1: support b = {x} by Def3;
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 PRE_POLY:52;
hence not b is empty by POLYNOM2:def 1; :: thesis: verum