theorem Th21: :: TOPALG_5:21

for UL being Subset-Family of (Tunit_circle 2) st UL is Cover of (Tunit_circle 2) & UL is open holds
for Y being non empty TopSpace
for F being continuous Function of [:Y,I[01]:],(Tunit_circle 2)
for y being Point of Y ex T being non empty FinSequence of REAL st
( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of (Tunit_circle 2) st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )