:: deftheorem Def2 defines Rule PROOFS_1:def 2 :
for Fml being set
for b₂ being Rule holds
( b₂ is Rule of Fml iff ( dom b₂ c= Fin Fml & rng b₂ c= Fml ) );