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