let
X
be
set
;
:: thesis:
(
X
=
F
_V
implies
X
is
empty
)
assume
A1
:
X
=
F
_V
;
:: thesis:
X
is
empty
dom
(
F
_V
)
is
empty
by
Def10
;
hence
X
is
empty
by
A1
;
:: thesis:
verum