theorem :: FIN_TOPO:15

for FT being non empty finite filled RelStr
for A being Subset of FT holds
( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )