let C1 be non empty set ; :: thesis: for F, G being Membership_Func of C1 st ( for x being set st x in C1 holds
F . x <= G . x ) holds
upper_bound (rng F) <= upper_bound (rng G)
let F, G be Membership_Func of C1; :: thesis: ( ( for x being set st x in C1 holds
F . x <= G . x ) implies upper_bound (rng F) <= upper_bound (rng G) )
rng F is real-bounded by Th1;
then A1: rng F is bounded_above by XXREAL_2:def 11;
assume A2: for c being set st c in C1 holds
F . c <= G . c ; :: thesis: upper_bound (rng F) <= upper_bound (rng G)
A3: for s being Real st 0 < s holds
ex y being set st
( y in dom F & (upper_bound (rng F)) - s <= G . y )

proof

let s be Real; :: thesis: ( 0 < s implies ex y being set st
( y in dom F & (upper_bound (rng F)) - s <= G . y ) )
assume 0 < s ; :: thesis: ex y being set st
( y in dom F & (upper_bound (rng F)) - s <= G . y )
then consider r being Real such that
A4: r in rng F and
A5: (upper_bound (rng F)) - s < r by A1, SEQ_4:def 1;
consider y being object such that
A6: y in dom F and
A7: r = F . y by A4, FUNCT_1:def 3;
r <= G . y by A2, A6, A7;
hence ex y being set st
( y in dom F & (upper_bound (rng F)) - s <= G . y ) by A5, A6, XXREAL_0:2; :: thesis: verum

end;

for s being Real st 0 < s holds
(upper_bound (rng F)) - s <= upper_bound (rng G)

proof

let s be Real; :: thesis: ( 0 < s implies (upper_bound (rng F)) - s <= upper_bound (rng G) )
assume 0 < s ; :: thesis: (upper_bound (rng F)) - s <= upper_bound (rng G)
then consider y being set such that
A8: y in dom F and
A9: (upper_bound (rng F)) - s <= G . y by A3;
y in C1 by A8;
then y in dom G by FUNCT_2:def 1;
then G . y <= upper_bound (rng G) by Th1;
hence (upper_bound (rng F)) - s <= upper_bound (rng G) by A9, XXREAL_0:2; :: thesis: verum

end;

hence upper_bound (rng F) <= upper_bound (rng G) by XREAL_1:57; :: thesis: verum