Description: Restricted for-all over a triple cross product with explicit substitution. (Contributed by Scott Fenton, 22-Aug-2024)