let X be Subset of REAL; :: thesis: ( X is open & X is bounded_above implies not upper_bound X in X )
assume that
A1: X is open and
A2: X is bounded_above ; :: thesis: not upper_bound X in X
assume upper_bound X in X ; :: thesis: contradiction
then consider N being Neighbourhood of upper_bound X such that
A3: N c= X by A1, Th18;
consider t being Real such that
A4: t > 0 and
A5: N = ].((upper_bound X) - t),((upper_bound X) + t).[ by Def6;
A6: (upper_bound X) + (t / 2) > upper_bound X by A4, XREAL_1:29, XREAL_1:215;
A7: ((upper_bound X) + (t / 2)) + (t / 2) > (upper_bound X) + (t / 2) by A4, XREAL_1:29, XREAL_1:215;
(upper_bound X) - t < upper_bound X by A4, XREAL_1:44;
then (upper_bound X) - t < (upper_bound X) + (t / 2) by A6, XXREAL_0:2;
then (upper_bound X) + (t / 2) in { s where s is Real : ( (upper_bound X) - t < s & s < (upper_bound X) + t ) } by A7;
hence contradiction by A2, A3, A5, A6, SEQ_4:def 1; :: thesis: verum