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