set S = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ;

now :: thesis: for x being object st x in { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } holds
x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))

let x be object ; :: thesis: ( x in { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } implies x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) )
assume x in { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ; :: thesis: x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
then ex v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( x = v & v is invertible ) ;
hence x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ; :: thesis: verum

end;

then reconsider S = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } as Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by TARSKI:def 3;
S is open by Th3;
hence { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } is open Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ; :: thesis: verum