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
A1: x > 0 and
A2: x ** A is bounded_below ; :: thesis: A is bounded_below
A3: inf (x ** A) <> -infty by A2;
consider r being Real such that
A4: r in A by MEMBERED:9;

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

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

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of A
A6: x * r in x ** A by A4, MEMBER_1:193;
+infty is LowerBound of x ** A by A5, XXREAL_2:def 4;
hence 0 is LowerBound of A by A6, 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 ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not z in A or r / x <= z )
assume A7: z in A ; :: thesis: r / x <= z
(x ") ** (x ** A) = A by A1, Th1;
then consider s being Real such that
A8: s in x ** A and
A9: z = (x ") * s by A7, INTEGRA2:39;
r / x <= s / x by A1, A8, XREAL_1:72, XXREAL_2:3;
hence r / x <= z by A9; :: thesis: verum

end;

end;