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

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