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, Th39;
consider t being real number such that
A4: ( t > 0 & N = ].((upper_bound X) - t),((upper_bound X) + t).[ ) by Def7;
A5: t / 2 > 0 by A4, XREAL_1:217;
then A6: (upper_bound X) + (t / 2) > upper_bound X by XREAL_1:31;
A7: ((upper_bound X) + (t / 2)) + (t / 2) > (upper_bound X) + (t / 2) by A5, XREAL_1:31;
(upper_bound X) - t < upper_bound X by A4, XREAL_1:46;
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, A4, A6, SEQ_4:def 4; :: thesis: verum