theorem Th3: :: LOPBAN_2:3

for X being RealNormSpace holds id the carrier of X is Lipschitzian LinearOperator of X,X