let P, R be Relation; :: thesis: ( rng R c= rng P & P is positive-yielding implies R is positive-yielding )
assume A1: ( rng R c= rng P & P is positive-yielding ) ; :: thesis: R is positive-yielding
let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in proj2 R or not r <= 0 )
thus ( not r in proj2 R or not r <= 0 ) by A1, PARTFUN3:def 1; :: thesis: verum