let r be Real; :: thesis: for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds
upper_bound (r ** X) = r * (lower_bound X)
let X be non empty Subset of REAL; :: thesis: ( X is bounded_below & r <= 0 implies upper_bound (r ** X) = r * (lower_bound X) )
assume that
A1: X is bounded_below and
A2: r <= 0 ; :: thesis: upper_bound (r ** X) = r * (lower_bound X)
A3: for a being Real st a in r ** X holds
r * (lower_bound X) >= a

proof

let a be Real; :: thesis: ( a in r ** X implies r * (lower_bound X) >= a )
assume a in r ** X ; :: thesis: r * (lower_bound X) >= a
then a in { (r * x) where x is Real : x in X } by Th8;
then consider x being Real such that
A4: a = r * x and
A5: x in X ;
lower_bound X <= x by A1, A5, SEQ_4:def 2;
hence r * (lower_bound X) >= a by A2, A4, XREAL_1:65; :: thesis: verum

end;

for b being Real st ( for a being Real st a in r ** X holds
a <= b ) holds
r * (lower_bound X) <= b

proof

consider x being Element of REAL such that
A6: x in X by SUBSET_1:4;
let b be Real; :: thesis: ( ( for a being Real st a in r ** X holds
a <= b ) implies r * (lower_bound X) <= b )
assume A7: for a being Real st a in r ** X holds
a <= b ; :: thesis: r * (lower_bound X) <= b
reconsider x = x as Real ;
r * x in { (r * y) where y is Real : y in X } by A6;
then A8: r * x in r ** X by Th8;

now :: thesis: r * (lower_bound X) <= b

per cases ( r = 0 or r < 0 ) by A2;

suppose r = 0 ; :: thesis: r * (lower_bound X) <= b

hence r * (lower_bound X) <= b by A7, A8; :: thesis: verum

end;

suppose A9: r < 0 ; :: thesis: r * (lower_bound X) <= b

for z being Real st z in X holds
z >= b / r

proof

let z be Real; :: thesis: ( z in X implies z >= b / r )
assume z in X ; :: thesis: z >= b / r
then r * z in { (r * y) where y is Real : y in X } ;
then r * z in r ** X by Th8;
hence z >= b / r by A7, A9, XREAL_1:78; :: thesis: verum

end;

then lower_bound X >= b / r by SEQ_4:43;
then r * (lower_bound X) <= (b / r) * r by A9, XREAL_1:65;
hence r * (lower_bound X) <= b by A9, XCMPLX_1:87; :: thesis: verum

end;

end;

end;

hence r * (lower_bound X) <= b ; :: thesis: verum

end;

hence upper_bound (r ** X) = r * (lower_bound X) by A3, SEQ_4:46; :: thesis: verum