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