let X be non empty Subset of ExtREAL ; :: thesis: sup (- X) = - (inf X)
set a = sup (- X);
set b = inf X;
A1: ( 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;
A2: ( 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;
A3: sup (- X) <= - (inf X)

proof

- (inf X) is UpperBound of - X by A2, Th31;
hence sup (- X) <= - (inf X) by XXREAL_2:def 3; :: thesis: verum

end;

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

proof

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

end;

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