Theorem Ordinal.lt_wf

Modification history