let C be non empty set ; :: thesis: for a, b being Element of REAL
for f being PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds
for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )

let a, b be Element of REAL ; :: thesis: for f being PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds
for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )

let f be PartFunc of C,REAL; :: thesis: ( rng f c= [.a,b.] & a <= b implies for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b ) )

assume that
A1: rng f c= [.a,b.] and
A2: a <= b ; :: thesis: for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )

for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )
proof
reconsider A = [.a,b.] as non empty closed_interval Subset of REAL by ;
let x be Element of C; :: thesis: ( x in dom f implies ( a <= f . x & f . x <= b ) )
A = [.(),().] by INTEGRA1:4;
then A3: ( a = lower_bound A & b = upper_bound A ) by INTEGRA1:5;
assume x in dom f ; :: thesis: ( a <= f . x & f . x <= b )
then f . x in rng f by FUNCT_1:def 3;
hence ( a <= f . x & f . x <= b ) by ; :: thesis: verum
end;
hence for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b ) ; :: thesis: verum