theorem Th18: :: LOPBAN_2:18

for X being non trivial RealNormSpace holds (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1