set
x
= the
Element
of
X
;
reconsider
y
= the
Element
of
X
as
Element
of
L
;
reconsider
Z
=
{
y
}
as
finite
Subset
of
X
by
ZFMISC_1:31
;
ex_inf_of
Z
,
L
by
YELLOW_0:38
;
then
"/\"
(
Z
,
L
)
in
fininfs
X
;
hence
not
fininfs
X
is
empty
;
:: thesis:
verum