let X be non empty Subset of ExtREAL ; :: thesis: inf (- X) = - (sup X)
set a = inf (- X);
set b = sup X;
A1: ( inf (- X) is LowerBound of - X & ( for y being R_eal st y is LowerBound of - X holds
y <= inf (- X) ) ) by XXREAL_2:def 4;
A2: ( sup X is UpperBound of X & ( for y being R_eal st y is UpperBound of X holds
sup X <= y ) ) by XXREAL_2:def 3;
A3: inf (- X) <= - (sup X)

proof

- (inf (- X)) is UpperBound of - (- X) by A1, Th31;
then - (inf (- X)) is UpperBound of X by Th22;
then sup X <= - (inf (- X)) by XXREAL_2:def 3;
then - (- (inf (- X))) <= - (sup X) by XXREAL_3:40;
hence inf (- X) <= - (sup X) ; :: thesis: verum

end;

- (sup X) <= inf (- X)

proof

- (sup X) is LowerBound of - X by A2, Th30;
hence - (sup X) <= inf (- X) by XXREAL_2:def 4; :: thesis: verum

end;

hence inf (- X) = - (sup X) by A3, XXREAL_0:1; :: thesis: verum