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

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