theorem
Th12
:
:: SUPINF_2:13
for
X
being non
empty
Subset
of
ExtREAL
for
a
being
R_eal
holds
(
a
is
LowerBound
of
X
iff

a
is
UpperBound
of

X
)