:: deftheorem Def4 defines Formula-finset PROOFS_1:def 4 :
for Fml being set
for b₂ being Formula-finset holds
( b₂ is Formula-finset of Fml iff b₂ c= Fml );