reconsider f = {} as Function ;
reconsider f = f as PartFunc of X,REAL by RELSET_1:25;
take f ; :: thesis: f is nonnegative
let x be Element of ExtREAL ; :: according to SUPINF_2:def 15,SUPINF_2:def 22 :: thesis: ( not x in proj2 f or 0. <= x )
thus ( not x in proj2 f or 0. <= x ) ; :: thesis: verum