let b be bag of ; :: thesis: b = EmptyBag {}
set n = {} ;
A1: for b being bag of holds b = {}

proof

let b be bag of ; :: thesis: b = {}
b in Bags {} by POLYNOM1:def 14;
hence b = {} by POLYNOM1:55, TARSKI:def 1; :: thesis: verum

end;

then EmptyBag {} = {} ;
hence b = EmptyBag {} by A1; :: thesis: verum