:: deftheorem Def5 defines Formula-sequence PROOFS_1:def 5 :
for Fml being set
for b₂ being Formula-sequence holds
( b₂ is Formula-sequence of Fml iff b₂ is FinSequence of Fml );