rng
f
c/=
{
{}
}
by
RELAT_1:def 15
;
then
consider
x
being
object
such that
A1
: (
x
in
rng
f
&
x
nin
{
{}
}
) ;
reconsider
x
=
x
as
set
by
TARSKI:1
;
(
x
<>
{}
&
x
c=
Union
f
)
by
A1
,
TARSKI:def 1
,
ZFMISC_1:74
;
hence
not
Union
f
is
empty
;
:: thesis:
verum