:: deftheorem Def6 defines Finf FINTOPO3:def 6 :
for T being non empty RelStr
for A being Subset of T
for b₃ being sequence of (bool the carrier of T) holds
( b₃ = Finf A iff ( ( for n being Nat
for B being Subset of T st B = b₃ . n holds
b₃ . (n + 1) = B ^f ) & b₃ . 0 = A ) );