theorem
Th14
:
:: SUPINF_2:15
for
X
being non
empty
Subset
of
ExtREAL
holds
sup
(

X
)
=

(
inf
X
)