theorem Th13: :: TOPMETR3:13

for X being non empty MetrSpace
for f being Function of I[01],(TopSpaceMetr X)
for F1, F2 being Subset of (TopSpaceMetr X)
for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds
ex r being Real st
( r1 <= r & r <= r2 & f . r in F1 /\ F2 )