theorem :: NFCONT_1:44

for S being RealNormSpace
for Y being Subset of S holds id Y is_Lipschitzian_on Y