set
x
= the
Element
of
X
;
reconsider
x9
= the
Element
of
X
as
Element
of
L
;
x9
<=
x9
;
hence
not
uparrow
X
is
empty
by
Def16
;
:: thesis:
verum