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