Description: One direction of sbn , using fewer axioms. Compare 19.2 . (Contributed by Steven Nguyen, 18-Aug-2023)