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