let T, T1 be non empty TopSpace; :: thesis: for f being continuous Function of T,T1 st T1 is T_1 holds
for w being set st w in the carrier of (T_1-reflex T) holds
ex z being Element of T1 st
( z in rng f & w c= f " {z} )
let f be continuous Function of T,T1; :: thesis: ( T1 is T_1 implies for w being set st w in the carrier of (T_1-reflex T) holds
ex z being Element of T1 st
( z in rng f & w c= f " {z} ) )
assume A1: T1 is T_1 ; :: thesis: for w being set st w in the carrier of (T_1-reflex T) holds
ex z being Element of T1 st
( z in rng f & w c= f " {z} )
let w be set ; :: thesis: ( w in the carrier of (T_1-reflex T) implies ex z being Element of T1 st
( z in rng f & w c= f " {z} ) )
assume w in the carrier of (T_1-reflex T) ; :: thesis: ex z being Element of T1 st
( z in rng f & w c= f " {z} )
then w in Intersection (Closed_Partitions T) by BORSUK_1:def 7;
then consider x being Element of T such that
A2: w = EqClass (x,(Intersection (Closed_Partitions T))) by EQREL_1:42;
reconsider x = x as Element of T ;
reconsider fx = f . x as Element of T1 ;
take fx ; :: thesis: ( fx in rng f & w c= f " {fx} )
dom f = the carrier of T by FUNCT_2:def 1;
hence ( fx in rng f & w c= f " {fx} ) by A1, A2, Th6, FUNCT_1:def 3; :: thesis: verum