let b be bag of X; :: thesis: ( b is univariate implies not b is V3() )

assume b is univariate ; :: thesis: b is V3()

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 V3() by PRE_POLY:def 18; :: thesis: verum

assume b is univariate ; :: thesis: b is V3()

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 V3() by PRE_POLY:def 18; :: thesis: verum