let X be Subset of REAL; ( 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
; not upper_bound X in X
assume
upper_bound X in X
; 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; verum