set n = {} ;

let b be bag of {} ; :: thesis: b = EmptyBag {}

A1: for b being bag of {} holds b = {}

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

let b be bag of {} ; :: thesis: b = EmptyBag {}

A1: for b being bag of {} holds b = {}

proof

then
EmptyBag {} = {}
;
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;b in Bags {} by PRE_POLY:def 12;

hence b = {} by PRE_POLY:51, TARSKI:def 1; :: thesis: verum

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