for n being Element of NAT
for e being Real
for g being Function of I[01],(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )