let R be ext-real-valued Relation; :: thesis: ( R is with_values_greater_or_equal_one implies R is positive-yielding )
assume A1: R is with_values_greater_or_equal_one ; :: thesis: R is positive-yielding
let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in rng R or not r <= 0 )
thus ( not r in rng R or not r <= 0 ) by A1; :: thesis: verum