let X be non empty Subset of ExtREAL; :: thesis: for a being R_eal holds

( a is LowerBound of X iff - a is UpperBound of - X )

let a be R_eal; :: thesis: ( a is LowerBound of X iff - a is UpperBound of - X )

for x being ExtReal st x in X holds

a <= x

( a is LowerBound of X iff - a is UpperBound of - X )

let a be R_eal; :: thesis: ( a is LowerBound of X iff - a is UpperBound of - X )

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

assume A3:
- a is UpperBound of - X
; :: thesis: a is LowerBound of Xassume A1:
a is LowerBound of X
; :: thesis: - a is UpperBound of - X

for x being ExtReal st x in - X holds

x <= - a

end;for x being ExtReal st x in - X holds

x <= - a

proof

hence
- a is UpperBound of - X
by XXREAL_2:def 1; :: thesis: verum
let x be ExtReal; :: thesis: ( x in - X implies x <= - a )

assume A2: x in - X ; :: thesis: x <= - a

reconsider x = x as Element of ExtREAL by XXREAL_0:def 1;

- x in - (- X) by A2;

then - (- x) <= - a by XXREAL_3:38, A1, XXREAL_2:def 2;

hence x <= - a ; :: thesis: verum

end;assume A2: x in - X ; :: thesis: x <= - a

reconsider x = x as Element of ExtREAL by XXREAL_0:def 1;

- x in - (- X) by A2;

then - (- x) <= - a by XXREAL_3:38, A1, XXREAL_2:def 2;

hence x <= - a ; :: thesis: verum

for x being ExtReal st x in X holds

a <= x

proof

hence
a is LowerBound of X
by XXREAL_2:def 2; :: thesis: verum
let x be ExtReal; :: thesis: ( x in X implies a <= x )

assume A4: x in X ; :: thesis: a <= x

reconsider x = x as Element of ExtREAL by XXREAL_0:def 1;

- x in - X by A4;

hence a <= x by XXREAL_3:38, A3, XXREAL_2:def 1; :: thesis: verum

end;assume A4: x in X ; :: thesis: a <= x

reconsider x = x as Element of ExtREAL by XXREAL_0:def 1;

- x in - X by A4;

hence a <= x by XXREAL_3:38, A3, XXREAL_2:def 1; :: thesis: verum