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 Th31;
then - (inf (- X)) is UpperBound of X by Th22;
then sup X <= - (inf (- X)) by XXREAL_2:def 3;
then A1: - (- (inf (- X))) <= - (sup X) by XXREAL_3:40;
sup X is UpperBound of X by XXREAL_2:def 3;
then - (sup X) is LowerBound of - X by Th30;
then - (sup X) <= inf (- X) by XXREAL_2:def 4;
hence inf (- X) = - (sup X) by A1, XXREAL_0:1; :: thesis: verum