let X be non empty set ; :: thesis: for Y being non empty Subset of ExtREAL

for F being Function of X,Y

for x being Element of X holds

( inf F <= F . x & F . x <= sup F )

let Y be non empty Subset of ExtREAL; :: thesis: for F being Function of X,Y

for x being Element of X holds

( inf F <= F . x & F . x <= sup F )

let F be Function of X,Y; :: thesis: for x being Element of X holds

( inf F <= F . x & F . x <= sup F )

let x be Element of X; :: thesis: ( inf F <= F . x & F . x <= sup F )

X = dom F by FUNCT_2:def 1;

then F . x in rng F by FUNCT_1:def 3;

hence ( inf F <= F . x & F . x <= sup F ) by XXREAL_2:3, XXREAL_2:4; :: thesis: verum

for F being Function of X,Y

for x being Element of X holds

( inf F <= F . x & F . x <= sup F )

let Y be non empty Subset of ExtREAL; :: thesis: for F being Function of X,Y

for x being Element of X holds

( inf F <= F . x & F . x <= sup F )

let F be Function of X,Y; :: thesis: for x being Element of X holds

( inf F <= F . x & F . x <= sup F )

let x be Element of X; :: thesis: ( inf F <= F . x & F . x <= sup F )

X = dom F by FUNCT_2:def 1;

then F . x in rng F by FUNCT_1:def 3;

hence ( inf F <= F . x & F . x <= sup F ) by XXREAL_2:3, XXREAL_2:4; :: thesis: verum