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 )