for X, Y being non trivial RealBanachSpace
for S being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st S = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } holds
S is open