Description: Demonstrate that there is never a "surprise" when using the allsome
quantifier restricted to a class, that is, it is never possible for the
consequent to be both always true and always false of the members of A
that satisfy the antecedent. This is the restricted counterpart of
als-no-surprise , and follows from it by dfrals2 . Note that this
needs no assumption that A is nonempty, because allsome requires a
member of A satisfying ph , and that member would have to satisfy
both ps and -. ps . The ordinary restricted "for all" requires no
such member and can be vacuously true, as shown in empty-surprise2 ;
that is the point of allsome. (Contributed by David A. Wheeler, 12-Jul-2026)