rng <*1*> = {1} by FINSEQ_1:38;
hence <*1*> is with_values_greater_or_equal_one by TARSKI:def 1; :: thesis: verum