Description: Obsolete version of r19.12 as of 19-May-2023. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 30-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)