let x be real number ; :: according to PARTFUN3:def 4 :: thesis: ( x in rng (X --> r) implies 0 <= x )
assume A1: x in rng (X --> r) ; :: thesis: 0 <= x
thus 0 <= x by A1, TARSKI:def 1; :: thesis: verum