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

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

hence contradiction by XREAL_1:145; :: thesis: verum

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

then
[/(inf Y)\] <= inf Y
by Def4;
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;assume x in X ; :: thesis: [/(inf Y)\] <= x

hence [/(inf Y)\] <= x by Th3, INT_1:65; :: thesis: verum

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

then
s + 1 <= s
by Def4;
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;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

hence contradiction by XREAL_1:145; :: thesis: verum