let X be non empty Subset of ExtREAL; :: thesis: for a being R_eal holds
( a is UpperBound of X iff - a is LowerBound of - X )
let a be R_eal; :: thesis: ( a is UpperBound of X iff - a is LowerBound of - X )

hereby :: thesis: ( - a is LowerBound of - X implies a is UpperBound of X )

assume A1: a is UpperBound of X ; :: thesis: - a is LowerBound of - X
for x being ExtReal st x in - X holds
- a <= x

proof

let x be ExtReal; :: thesis: ( x in - X implies - a <= x )
assume A2: x in - X ; :: thesis: - a <= x
reconsider x = x as Element of ExtREAL by XXREAL_0:def 1;
- x in - (- X) by A2;
then - a <= - (- x) by XXREAL_3:38, A1, XXREAL_2:def 1;
hence - a <= x ; :: thesis: verum

end;

hence - a is LowerBound of - X by XXREAL_2:def 2; :: thesis: verum

end;

assume A3: - a is LowerBound of - X ; :: thesis: a is UpperBound of X
for x being ExtReal st x in X holds
x <= a

proof

let x be ExtReal; :: thesis: ( x in X implies x <= a )
assume A4: x in X ; :: thesis: x <= a
reconsider x = x as Element of ExtREAL by XXREAL_0:def 1;
- x in - X by A4;
hence x <= a by XXREAL_3:38, A3, XXREAL_2:def 2; :: thesis: verum

end;

hence a is UpperBound of X by XXREAL_2:def 1; :: thesis: verum