let a be Point of (); :: thesis: upper_bound () = a `1
set X = proj1 .: ();
A1: now :: thesis: for r being Real st r in proj1 .: () holds
r <= a `1
let r be Real; :: thesis: ( r in proj1 .: () implies r <= a `1 )
assume r in proj1 .: () ; :: thesis: r <= a `1
then consider x being object such that
A2: x in the carrier of () and
A3: x in west_halfline a and
A4: r = proj1 . x by FUNCT_2:64;
reconsider x = x as Point of () by A2;
r = x `1 by ;
hence r <= a `1 by ; :: thesis: verum
end;
A5: now :: thesis: for s being Real st 0 < s holds
ex r being Real st
( r in proj1 .: () & (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 .: () & (a `1) - s < r ) )

assume 0 < s ; :: thesis: ex r being Real st
( r in proj1 .: () & (a `1) - s < r )

then A6: (a `1) - s < r - 0 by XREAL_1:15;
take r = r; :: thesis: ( r in proj1 .: () & (a `1) - s < r )
( a in west_halfline a & r = proj1 . a ) by ;
hence r in proj1 .: () by FUNCT_2:35; :: thesis: (a `1) - s < r
thus (a `1) - s < r by A6; :: thesis: verum
end;
proj1 .: () is bounded_above by Th5;
hence upper_bound () = a `1 by ; :: thesis: verum