set S = support (EmptyBag X);
assume not support (EmptyBag X) is empty ; :: thesis: contradiction
then (EmptyBag X) . the Element of support (EmptyBag X) <> 0 by Def7;
hence contradiction ; :: thesis: verum