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