let a be Point of (TOP-REAL 2); :: thesis: upper_bound (proj1 .: (west_halfline a)) = a `1
set X = proj1 .: (west_halfline a);

A1: now

let r be real number ; :: thesis: ( r in proj1 .: (west_halfline a) implies r <= a `1 )
assume r in proj1 .: (west_halfline a) ; :: thesis: r <= a `1
then consider x being set such that
A2: x in the carrier of (TOP-REAL 2) and
A3: x in west_halfline a and
A4: r = proj1 . x by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A2;
r = x `1 by A4, PSCOMP_1:def 28;
hence r <= a `1 by A3, TOPREAL1:def 15; :: thesis: verum

end;

A5: now

reconsider r = a `1 as real number ;
let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in proj1 .: (west_halfline a) & (a `1) - s < r ) )
assume 0 < s ; :: thesis: ex r being real number st
( r in proj1 .: (west_halfline a) & (a `1) - s < r )
then A6: (a `1) - s < r - 0 by XREAL_1:17;
take r = r; :: thesis: ( r in proj1 .: (west_halfline a) & (a `1) - s < r )
( a in west_halfline a & r = proj1 . a ) by PSCOMP_1:def 28, TOPREAL1:45;
hence r in proj1 .: (west_halfline a) by FUNCT_2:43; :: thesis: (a `1) - s < r
thus (a `1) - s < r by A6; :: thesis: verum

end;

proj1 .: (west_halfline a) is bounded_above by Th6;
hence upper_bound (proj1 .: (west_halfline a)) = a `1 by A1, A5, SEQ_4:def 4; :: thesis: verum