let f be non empty real-valued Function; :: thesis: ( f is empty-yielding implies not f is positive-yielding )
assume A1: f is empty-yielding ; :: thesis: not f is positive-yielding
take the Element of rng f ; :: according to PARTFUN3:def 1 :: thesis: ( the Element of rng f in rng f & the Element of rng f <= 0 )
thus ( the Element of rng f in rng f & the Element of rng f <= 0 ) by A1, RELAT_1:149; :: thesis: verum