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