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