:: deftheorem defines with_values_greater_or_equal_one NUMBER13:def 2 :
for R being ext-real-valued Relation holds
( R is with_values_greater_or_equal_one iff for r being ExtReal st r in rng R holds
r >= 1 );