let X be set ; :: thesis: support (EmptyBag X) = {}
assume support (EmptyBag X) <> {} ; :: thesis: contradiction
then reconsider S = support (EmptyBag X) as non empty set ;
set u = the Element of S;
(EmptyBag X) . the Element of S <> 0 by PRE_POLY:def 7;
hence contradiction by PRE_POLY:52; :: thesis: verum