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

set X = proj1 .: (west_halfline a);

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

set X = proj1 .: (west_halfline a);

A1: now :: thesis: for r being Real st r in proj1 .: (west_halfline a) holds

r <= a `1

r <= a `1

let r be Real; :: 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 object 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:64;

reconsider x = x as Point of (TOP-REAL 2) by A2;

r = x `1 by A4, PSCOMP_1:def 5;

hence r <= a `1 by A3, TOPREAL1:def 13; :: thesis: verum

end;assume r in proj1 .: (west_halfline a) ; :: thesis: r <= a `1

then consider x being object 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:64;

reconsider x = x as Point of (TOP-REAL 2) by A2;

r = x `1 by A4, PSCOMP_1:def 5;

hence r <= a `1 by A3, TOPREAL1:def 13; :: thesis: verum

A5: now :: thesis: for s being Real st 0 < s holds

ex r being Real st

( r in proj1 .: (west_halfline a) & (a `1) - s < r )

proj1 .: (west_halfline a) is bounded_above
by Th5;ex r being Real st

( r in proj1 .: (west_halfline a) & (a `1) - s < r )

reconsider r = a `1 as Real ;

let s be Real; :: thesis: ( 0 < s implies ex r being Real st

( r in proj1 .: (west_halfline a) & (a `1) - s < r ) )

assume 0 < s ; :: thesis: ex r being Real st

( r in proj1 .: (west_halfline a) & (a `1) - s < r )

then A6: (a `1) - s < r - 0 by XREAL_1:15;

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 5, TOPREAL1:38;

hence r in proj1 .: (west_halfline a) by FUNCT_2:35; :: thesis: (a `1) - s < r

thus (a `1) - s < r by A6; :: thesis: verum

end;let s be Real; :: thesis: ( 0 < s implies ex r being Real st

( r in proj1 .: (west_halfline a) & (a `1) - s < r ) )

assume 0 < s ; :: thesis: ex r being Real st

( r in proj1 .: (west_halfline a) & (a `1) - s < r )

then A6: (a `1) - s < r - 0 by XREAL_1:15;

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 5, TOPREAL1:38;

hence r in proj1 .: (west_halfline a) by FUNCT_2:35; :: thesis: (a `1) - s < r

thus (a `1) - s < r by A6; :: thesis: verum

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