let X be Subset of REAL ; :: thesis: ( X is open & X is bounded_below implies not lower_bound X in X )
assume that
A1: X is open and
A2: X is bounded_below ; :: thesis: not lower_bound X in X
assume lower_bound X in X ; :: thesis: contradiction
then consider N being Neighbourhood of lower_bound X such that
A3: N c= X by A1, Th39;
consider t being real number such that
A4: ( t > 0 & N = ].((lower_bound X) - t),((lower_bound X) + t).[ ) by Def7;
A5: t / 2 > 0 by A4, XREAL_1:217;
then A6: (lower_bound X) - (t / 2) < lower_bound X by XREAL_1:46;
A7: ((lower_bound X) - (t / 2)) - (t / 2) < (lower_bound X) - (t / 2) by A5, XREAL_1:46;
lower_bound X < (lower_bound X) + t by A4, XREAL_1:31;
then (lower_bound X) - (t / 2) < (lower_bound X) + t by A6, XXREAL_0:2;
then (lower_bound X) - (t / 2) in { s where s is Real : ( (lower_bound X) - t < s & s < (lower_bound X) + t ) } by A7;
hence contradiction by A2, A3, A4, A6, SEQ_4:def 5; :: thesis: verum