(
X
is
empty
or not
X
is
empty
) ;
hence
for
b
_{1}
being
Element
of
X
holds
b
_{1}
is
INT
-valued
by
Def6
,
SUBSET_1:def 1
;
:: thesis:
verum