let
X
be non
empty
set
;
:: thesis:
not for
Y
being
Element
of
Fin
X
holds
Y
is
empty
set
a
= the
Element
of
X
;
{.
the
Element
of
X
.}
is
Element
of
Fin
X
;
hence
not for
Y
being
Element
of
Fin
X
holds
Y
is
empty
;
:: thesis:
verum