:: deftheorem Def3 defines Formula PROOFS_1:def 3 :
for Fml being non empty set
for b₂ being Formula holds
( b₂ is Formula of Fml iff b₂ in Fml );