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 )