:: deftheorem Def5 defines Fin FINSUB_1:def 5 :
for A being set
for b₂ being preBoolean set holds
( b₂ = Fin A iff for X being set holds
( X in b₂ iff ( X c= A & X is finite ) ) );