consider e being Element of SetVal (V,(p => (q => r)));
e is Function-yielding ;
hence ex b₁ being Element of SetVal (V,(p => (q => r))) st b₁ is Function-yielding ; :: thesis: verum