let S be Subset of (Bags X); :: thesis: S is functional
let x be set ; :: according to FUNCT_1:def 13 :: thesis: ( not x in S or x is set )
thus ( not x in S or x is set ) by Def12; :: thesis: verum