let a be Point of (); :: thesis: lower_bound () = a `2
set X = proj2 .: ();
A1: now :: thesis: for r being Real st r in proj2 .: () holds
a `2 <= r
let r be Real; :: thesis: ( r in proj2 .: () implies a `2 <= r )
assume r in proj2 .: () ; :: thesis: a `2 <= r
then consider x being object such that
A2: x in the carrier of () and
A3: x in north_halfline a and
A4: r = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of () by A2;
r = x `2 by ;
hence a `2 <= r by ; :: thesis: verum
end;
A5: now :: thesis: for s being Real st 0 < s holds
ex r being Real st
( r in proj2 .: () & r < (a `2) + s )
reconsider r = a `2 as Real ;
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in proj2 .: () & r < (a `2) + s ) )

assume 0 < s ; :: thesis: ex r being Real st
( r in proj2 .: () & r < (a `2) + s )

then A6: r + 0 < (a `2) + s by XREAL_1:8;
take r = r; :: thesis: ( r in proj2 .: () & r < (a `2) + s )
( a in north_halfline a & r = proj2 . a ) by ;
hence r in proj2 .: () by FUNCT_2:35; :: thesis: r < (a `2) + s
thus r < (a `2) + s by A6; :: thesis: verum
end;
proj2 .: () is bounded_below by Th3;
hence lower_bound () = a `2 by ; :: thesis: verum