theorem :: NCFCONT1:115

for CNS being ComplexNormSpace
for Y being Subset of CNS holds id Y is_Lipschitzian_on Y