for T being non empty TopSpace
for n being Nat st n >= 1 & ( for S being TopSpace
for A being non empty closed Subset of T
for B being Subset of S st ex X being Subset of (TOP-REAL n) st
( X is compact & not X is boundary & X is convex & B,X are_homeomorphic ) holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f ) ) holds
T is normal