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

proof

let b be bag of {} ; :: thesis: b = {}
b in Bags {} by PRE_POLY:def 12;
hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis: verum

end;

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