now :: thesis: for x being set holds
( ( x in {{}} implies x is bag of {} ) & ( x is bag of {} implies x in {{}} ) )
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 2, RELAT_1:38, RELAT_1:def 18; :: thesis: verum
end;
assume x is bag of {} ; :: thesis: x in {{}}
then reconsider x9 = x as ManySortedSet of {} ;
x9 = {} ;
hence x in {{}} by TARSKI:def 1; :: thesis: verum
end;
hence Bags {} = {{}} by Def12; :: thesis: verum