take <*1*> ; :: thesis: <*1*> is with_values_greater_or_equal_one
thus <*1*> is with_values_greater_or_equal_one ; :: thesis: verum