for X being RealUnitarySpace
for f being Function of X,REAL st f is_Lipschitzian_on the carrier of X holds
f is_continuous_on the carrier of X