now

let x be set ; :: thesis: ( ( x in {{} } implies x is bag of {} ) & ( x is bag of {} implies x in {{} } ) )

hereby :: thesis: ( x is bag of {} implies x in {{} } )

assume x in {{} } ; :: thesis: x is bag of {}
then x = {} by TARSKI:def 1;
hence x is bag of {} by PARTFUN1:def 4, RELAT_1:60, RELAT_1:def 18; :: thesis: verum

end;

assume x is bag of {} ; :: thesis: x in {{} }
then reconsider x9 = x as ManySortedSet of {} ;
dom x9 = {} by PARTFUN1:def 4;
then x9 = {} ;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

hence Bags {} = {{} } by Def14; :: thesis: verum