Description: One direction of sb5 , provable from fewer axioms. Version of sb1 with a disjoint variable condition using fewer axioms. (Contributed by NM, 13-May-1993) (Revised by Wolf Lammen, 20-Jan-2024)