let C1 be non empty set ; :: thesis: for F being Membership_Func of C1 holds
( rng F is real-bounded & ( for x being set st x in dom F holds
F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds
F . x >= lower_bound (rng F) ) )
let F be Membership_Func of C1; :: thesis: ( rng F is real-bounded & ( for x being set st x in dom F holds
F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds
F . x >= lower_bound (rng F) ) )
A1: [.0,jj.] is non empty closed_interval Subset of REAL by MEASURE5:14;
A2: rng F c= [.0,1.] by RELAT_1:def 19;
then A3: rng F is real-bounded by A1, XXREAL_2:45;
A4: for x being set st x in dom F holds
F . x >= lower_bound (rng F)

proof

let x be set ; :: thesis: ( x in dom F implies F . x >= lower_bound (rng F) )
assume x in dom F ; :: thesis: F . x >= lower_bound (rng F)
then A5: F . x in rng F by FUNCT_1:def 3;
rng F is bounded_below by A3, XXREAL_2:def 11;
hence F . x >= lower_bound (rng F) by A5, SEQ_4:def 2; :: thesis: verum

end;

for x being set st x in dom F holds
F . x <= upper_bound (rng F)

proof

let x be set ; :: thesis: ( x in dom F implies F . x <= upper_bound (rng F) )
assume x in dom F ; :: thesis: F . x <= upper_bound (rng F)
then A6: F . x in rng F by FUNCT_1:def 3;
rng F is bounded_above by A3, XXREAL_2:def 11;
hence F . x <= upper_bound (rng F) by A6, SEQ_4:def 1; :: thesis: verum

end;

hence ( rng F is real-bounded & ( for x being set st x in dom F holds
F . x <= upper_bound (rng F) ) & ( for x being set st x in dom F holds
F . x >= lower_bound (rng F) ) ) by A2, A1, A4, XXREAL_2:45; :: thesis: verum