set
a
= the
Element
of
X
;
[
the
Element
of
X
, the
Element
of
X
]
in
RelIncl
X
by
Def1
;
hence
not
RelIncl
X
is
empty
;
:: thesis:
verum