let n be set ; :: thesis: support (EmptyBag n) = {}
assume not support (EmptyBag n) = {} ; :: thesis: contradiction
then consider x being set such that
A1: x in support (EmptyBag n) by XBOOLE_0:def 1;
(EmptyBag n) . x <> 0 by A1, PRE_POLY:def 7;
hence contradiction by PRE_POLY:52; :: thesis: verum