theorem
proved
diameter_support_simple_representatives_from_ordered_representatives
show as:
diameter_support_simple_representatives_from_ordered_representatives