:: deftheorem Def3 defines Sub_of_Fin COHSP_1:def 3 :
for X being set
for b₂ being Subset of X holds
( b₂ = Sub_of_Fin X iff for x being set holds
( x in b₂ iff ( x in X & x is finite ) ) );