Theorem exists_lt_of_ciInf_lt

Modification history