let X be non empty Subset of ExtREAL; :: thesis: sup (- X) = - (inf X)
set a = sup (- X);
set b = inf X;
sup (- X) is UpperBound of - X by XXREAL_2:def 3;
then - (sup (- X)) is LowerBound of - (- X) by Th11;
then A1: - (inf X) <= - (- (sup (- X))) by XXREAL_3:38, XXREAL_2:def 4;
inf X is LowerBound of X by XXREAL_2:def 4;
then - (inf X) is UpperBound of - X by Th12;
then sup (- X) <= - (inf X) by XXREAL_2:def 3;
hence sup (- X) = - (inf X) by A1, XXREAL_0:1; :: thesis: verum