let X be without_zero Subset of REAL; :: thesis: ( X is closed & X is bounded implies Inv X is closed )
assume that
A1: X is closed and
A2: X is bounded ; :: thesis: Inv X is closed
let s1 be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not proj2 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 set ; :: 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 set 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

assume not s1 is non-zero ; :: thesis: contradiction
then ex n being Element of NAT st s1 . n = 0 by SEQ_1:5;
hence contradiction by A8, FUNCT_2:4; :: thesis: verum

end;

A10: now

A11: rng (s1 ") c= X

proof

let y be set ; :: 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 set such that
A12: x in dom (s1 ") and
A13: y = (s1 ") . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A12;
s1 . x in rng s1 by FUNCT_2:4;
then 1 / (s1 . x) in Inv (Inv X) by A3;
hence y in X by A13, VALUED_1:10; :: thesis: verum

end;

assume lim s1 = 0 ; :: thesis: contradiction
then not s1 " is bounded by A4, A9, Th74;
then not rng (s1 ") is bounded by Th75;
hence contradiction by A2, A11, XXREAL_2:45; :: thesis: verum

end;

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