let A be non empty Subset of REAL ; :: thesis: for x being Real st x > 0 & x ** A is bounded_below holds
A is bounded_below
let x be Real; :: thesis: ( x > 0 & x ** A is bounded_below implies A is bounded_below )
assume that
Z1: x > 0 and
Z2: x ** A is bounded_below ; :: thesis: A is bounded_below
consider r being real number such that
W: r in A by MEMBERED:9;
R: inf (x ** A) <> -infty by Z2, XXREAL_2:78;

per cases ( inf (x ** A) = +infty or inf (x ** A) in REAL ) by R, XXREAL_0:14;

suppose S: inf (x ** A) = +infty ; :: thesis: A is bounded_below

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of A
T: +infty is LowerBound of x ** A by S, XXREAL_2:def 4;
x * r in x ** A by W, INTEGRA2:def 2;
hence 0 is LowerBound of A by T, XXREAL_0:4, XXREAL_2:def 2; :: thesis: verum

end;

suppose inf (x ** A) in REAL ; :: thesis: A is bounded_below

then reconsider r = inf (x ** A) as Real ;
take r / x ; :: according to XXREAL_2:def 9 :: thesis: r / x is LowerBound of A
let z be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not z in A or r / x <= z )
assume Z: z in A ; :: thesis: r / x <= z
then reconsider z1 = z as Real ;
(x " ) ** (x ** A) = A by Z1, Th2;
then consider s being Real such that
W1: s in x ** A and
W2: z = (x " ) * s by Z, INTEGRA2:def 2;
r / x <= s / x by Z1, W1, XREAL_1:74, XXREAL_2:3;
hence r / x <= z by W2; :: thesis: verum

end;

end;