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