Theorem sInf_le_sInf_of_forall_exists_le

Modification history