theorem
:: BHSP_6:9
for
X
being
RealUnitarySpace
for
Y
being
finite
Subset
of
X
st not
Y
is
empty
holds
Y
is
summable_set