let R be Relation; :: thesis: ( R is X -valued implies R is positive-yielding )
assume A1: R is X -valued ; :: 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, Def2; :: thesis: verum