let X be Subset of REAL; :: thesis:
assume that
A1: X <> {} and
A2: X is closed and
A3: X is bounded_above and
A4: not upper_bound X in X ; :: thesis:
set s1 = upper_bound X;
defpred S₁[ Element of NAT , Element of REAL ] means ex q being Real st
( q = $2 & q in X & (upper_bound X) - q < 1 / ($1 + 1) );
A5: for n being Element of NAT ex p being Element of REAL st S₁[n,p]

let n be Element of NAT ; :: thesis:
0 < (n + 1) " ;
then 0 < 1 / (n + 1) by XCMPLX_1:215;
then consider t being Real such that
A6: t in X and
A7: (upper_bound X) - (1 / (n + 1)) < t by A1, A3, SEQ_4:def 1;
take t ; :: thesis:
upper_bound X < t + (1 / (n + 1)) by A7, XREAL_1:19;
then (upper_bound X) - t < 1 / (n + 1) by XREAL_1:19;
hence ( t is set & t is Element of REAL & S₁[n,t] ) by A6; :: thesis:

end;

consider f being sequence of REAL such that
A8: for n being Element of NAT holds S₁[n,f . n] from FUNCT_2:sch 3(A5);

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A11, FUNCT_2:def 1;
f . y in X by A9;
hence x in X by A12; :: thesis:

end;

end;