Theorem sup_lt_sup_of_lt_of_inf_le_inf

Modification history