let b be bag of 0 ; :: thesis: ( dom b = {} & b = EmptyBag {} & rng b = 0 & EmptyBag {} = {} --> 0 & Bags {} = {(EmptyBag {})} )
Bags {} = {(EmptyBag {})}

proof

for o being object st o in Bags {} holds
o in {(EmptyBag {})}

proof

let o be object ; :: thesis: ( o in Bags {} implies o in {(EmptyBag {})} )
assume o in Bags {} ; :: thesis: o in {(EmptyBag {})}
then o = EmptyBag {} ;
hence o in {(EmptyBag {})} by TARSKI:def 1; :: thesis: verum

end;

then Bags {} c= {(EmptyBag {})} ;
hence Bags {} = {(EmptyBag {})} ; :: thesis: verum

end;

hence ( dom b = {} & b = EmptyBag {} & rng b = 0 & EmptyBag {} = {} --> 0 & Bags {} = {(EmptyBag {})} ) ; :: thesis: verum