let A be non empty Subset of REAL; :: thesis: for x being Real st x > 0 & x ** A is bounded_above holds
A is bounded_above
let x be Real; :: thesis: ( x > 0 & x ** A is bounded_above implies A is bounded_above )
assume that
A1: x > 0 and
A2: x ** A is bounded_above ; :: thesis: A is bounded_above
A3: sup (x ** A) <> +infty by A2;
consider r being Real such that
A4: r in A by MEMBERED:9;

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

suppose A5: sup (x ** A) = -infty ; :: thesis: A is bounded_above

take 0 ; :: according to XXREAL_2:def 10 :: thesis: 0 is UpperBound of A
A6: x * r in x ** A by A4, MEMBER_1:193;
-infty is UpperBound of x ** A by A5, XXREAL_2:def 3;
hence 0 is UpperBound of A by A6, XXREAL_0:6, XXREAL_2:def 1; :: thesis: verum

end;

suppose sup (x ** A) in REAL ; :: thesis: A is bounded_above

then reconsider r = sup (x ** A) as Real ;
take r / x ; :: according to XXREAL_2:def 10 :: thesis: r / x is UpperBound of A
let z be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not z in A or z <= r / x )
assume A7: z in A ; :: thesis: z <= r / x
(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;
s <= r by A8, XXREAL_2:4;
then s / x <= r / x by A1, XREAL_1:72;
hence z <= r / x by A9; :: thesis: verum

end;

end;