let x be set ; :: according to FUNCT_1:def 19 :: 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