theorem Th13: :: SUPINF_2:14

for X being non empty Subset of ExtREAL holds inf (- X) = - (sup X)