Theorem directed_of_inf

Modification history