let r be ExtReal; :: thesis: ( <*r*> is with_values_greater_or_equal_one implies r >= 1 )
rng <*r*> = {r} by FINSEQ_1:38;
then r in rng <*r*> by TARSKI:def 1;
hence ( <*r*> is with_values_greater_or_equal_one implies r >= 1 ) ; :: thesis: verum