for X being without_zero Subset of REAL st X is closed & X is real-bounded holds
Inv X is closed