let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in SetVal (V,(p => q)) or x is set )
assume x in SetVal (V,(p => q)) ; :: thesis: x is set
then x in Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2;
hence x is set ; :: thesis: verum