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 )
hereby :: thesis: ( - a is UpperBound of - X implies a is LowerBound of X )
assume A1: 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 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;
hence - a is UpperBound of - X by XXREAL_2:def 1; :: thesis: verum
end;
assume A3: - 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 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;
hence a is LowerBound of X by XXREAL_2:def 2; :: thesis: verum