let X be integer-membered non empty set ; :: thesis: ( X is bounded_below implies X is left_end )
assume X is bounded_below ; :: thesis: X is left_end
then reconsider Y = X as integer-membered non empty bounded_below set ;
set s = inf Y;
A1: [/(inf Y)\] >= inf Y by INT_1:def 7;
[/(inf Y)\] is LowerBound of X
proof
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies [/(inf Y)\] <= x )
assume x in X ; :: thesis: [/(inf Y)\] <= x
hence [/(inf Y)\] <= x by Th3, INT_1:65; :: thesis: verum
end;
then [/(inf Y)\] <= inf Y by Def4;
then reconsider s = inf Y as Integer by A1, XXREAL_0:1;
assume A2: not inf X in X ; :: according to XXREAL_2:def 5 :: thesis: contradiction
s + 1 is LowerBound of X
proof
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies s + 1 <= x )
assume A3: x in X ; :: thesis: s + 1 <= x
then reconsider i = x as Integer ;
i >= s by A3, Th3;
then s < i by A2, A3, XXREAL_0:1;
hence s + 1 <= x by INT_1:7; :: thesis: verum
end;
then s + 1 <= s by Def4;
hence contradiction by XREAL_1:145; :: thesis: verum