Theorem nonemptyFinLinOrdCat_dual_comp_forget_to_linOrdCat

Modification history