Description: Alternate proof of ab0 , shorter but using more axioms. (Contributed by BJ, 19-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)