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, Th18;
consider t being Real such that
A4: t > 0 and
A5: N = ].((lower_bound X) - t),((lower_bound X) + t).[ by Def6;
A6: (lower_bound X) - (t / 2) < lower_bound X by A4, XREAL_1:44, XREAL_1:215;
A7: ((lower_bound X) - (t / 2)) - (t / 2) < (lower_bound X) - (t / 2) by A4, XREAL_1:44, XREAL_1:215;
lower_bound X < (lower_bound X) + t by A4, XREAL_1:29;
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, A5, A6, SEQ_4:def 2; :: thesis: verum