Description: Alternative shorter proof of sbralie dependent on ax-ext . (Contributed by NM, 5-Sep-2004) (New usage is discouraged.) (Proof modification is discouraged.)