Description: Obsolete version of r19.21bi as of 11-Jun-2023. (Contributed by NM, 20-Nov-1994) (Proof shortened by Wolf Lammen, 1-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)