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