set
x
= the
Element
of
X
;
F
.
the
Element
of
X
in
rng
F
by
FUNCT_2:4
;
hence
rng
F
is non
empty
Subset
of
ExtREAL
by
XBOOLE_1:1
;
:: thesis:
verum