:: deftheorem Def12 defines Bags PRE_POLY:def 12 :
for X, b₂ being set holds
( b₂ = Bags X iff for x being set holds
( x in b₂ iff x is bag of X ) );