take id N ; :: thesis: id N is greater_or_equal_to_id
thus id N is greater_or_equal_to_id by Th4; :: thesis: verum