Description: Obsolete version of ominf as of 2-Jan-2025. (Contributed by NM, 2-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)