let X be without_zero Subset of REAL; :: thesis: ( X is closed & X is real-bounded implies Inv X is closed )
assume that
A1: X is closed and
A2: X is real-bounded ; :: thesis: Inv X is closed
let s1 be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not rng s1 c= Inv X or not s1 is convergent or lim s1 in Inv X )
assume that
A3: rng s1 c= Inv X and
A4: s1 is convergent ; :: thesis: lim s1 in Inv X
A5: rng (s1 ") c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s1 ") or x in X )
assume x in rng (s1 ") ; :: thesis: x in X
then consider n being object such that
A6: n in dom (s1 ") and
A7: x = (s1 ") . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A6;
s1 . n in rng s1 by FUNCT_2:4;
then 1 / (s1 . n) in Inv (Inv X) by A3;
hence x in X by A7, VALUED_1:10; :: thesis: verum

end;

A8: not 0 in rng s1 by A3;

A9: now :: thesis: s1 is non-zero

assume not s1 is non-zero ; :: thesis: contradiction
then consider n being Nat such that
A10: s1 . n = 0 by SEQ_1:5;
n in NAT by ORDINAL1:def 12;
hence contradiction by A8, FUNCT_2:4, A10; :: thesis: verum

end;

A11: now :: thesis: not lim s1 = 0

A12: rng (s1 ") c= X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (s1 ") or y in X )
assume y in rng (s1 ") ; :: thesis: y in X
then consider x being object such that
A13: x in dom (s1 ") and
A14: y = (s1 ") . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A13;
s1 . x in rng s1 by FUNCT_2:4;
then 1 / (s1 . x) in Inv (Inv X) by A3;
hence y in X by A14, VALUED_1:10; :: thesis: verum

end;

assume lim s1 = 0 ; :: thesis: contradiction
then not s1 " is bounded by A4, A9, Th38;
then not rng (s1 ") is real-bounded by Th39;
hence contradiction by A2, A12, XXREAL_2:45; :: thesis: verum

end;

then s1 " is convergent by A4, A9, SEQ_2:21;
then lim (s1 ") in X by A1, A5;
then 1 / (lim s1) in X by A4, A9, A11, SEQ_2:22;
then 1 / (1 / (lim s1)) in Inv X ;
hence lim s1 in Inv X ; :: thesis: verum