theorem
Th11
:
:: SUPINF_2:12
for
X
being non
empty
Subset
of
ExtREAL
for
a
being
R_eal
holds
(
a
is
UpperBound
of
X
iff

a
is
LowerBound
of

X
)