let x be Real; :: according to PARTFUN3:def 3 :: thesis: ( x in rng (X --> r) implies 0 >= x )

assume x in rng (X --> r) ; :: thesis: 0 >= x

hence 0 >= x by TARSKI:def 1; :: thesis: verum

assume x in rng (X --> r) ; :: thesis: 0 >= x

hence 0 >= x by TARSKI:def 1; :: thesis: verum