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 x' = x as ManySortedSet of ;
dom x' = {} by PARTFUN1:def 4;
then x' = {} ;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

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