theorem LM50: :: LOPBAN13:12

for X, Y being non trivial RealBanachSpace
for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
( 0 < ||.u.|| & 0 < ||.(Inv u).|| )