let C1 be non empty set ; :: thesis: for F being Membership_Func of C1 holds
( rng F is bounded & ( for x being set st x in dom F holds
F . x <= sup (rng F) ) & ( for x being set st x in dom F holds
F . x >= inf (rng F) ) )
let F be Membership_Func of C1; :: thesis: ( rng F is bounded & ( for x being set st x in dom F holds
F . x <= sup (rng F) ) & ( for x being set st x in dom F holds
F . x >= inf (rng F) ) )
A1: rng F is bounded

proof

A2: rng F c= [.0 ,1.] by RELAT_1:def 19;
[.0 ,1.] is closed-interval Subset of REAL by INTEGRA1:def 1;
hence rng F is bounded by A2, XXREAL_2:45; :: thesis: verum

end;

A3: for x being set st x in dom F holds
F . x <= sup (rng F)

proof

let x be set ; :: thesis: ( x in dom F implies F . x <= sup (rng F) )
assume x in dom F ; :: thesis: F . x <= sup (rng F)
then A4: F . x in rng F by FUNCT_1:def 5;
rng F is bounded_above by A1, XXREAL_2:def 11;
hence F . x <= sup (rng F) by A4, SEQ_4:def 4; :: thesis: verum

end;

for x being set st x in dom F holds
F . x >= inf (rng F)

proof

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

end;

hence ( rng F is bounded & ( for x being set st x in dom F holds
F . x <= sup (rng F) ) & ( for x being set st x in dom F holds
F . x >= inf (rng F) ) ) by A1, A3; :: thesis: verum