theorem
proved
distinct_diameter_representatives_meet_simply_from_cases
show as:
distinct_diameter_representatives_meet_simply_from_cases