let a be Point of (TOP-REAL 2); :: thesis: lower_bound (proj2 .: (north_halfline a)) = a `2

set X = proj2 .: (north_halfline a);

hence lower_bound (proj2 .: (north_halfline a)) = a `2 by A1, A5, SEQ_4:def 2; :: thesis: verum

set X = proj2 .: (north_halfline a);

A1: now :: thesis: for r being Real st r in proj2 .: (north_halfline a) holds

a `2 <= r

a `2 <= r

let r be Real; :: thesis: ( r in proj2 .: (north_halfline a) implies a `2 <= r )

assume r in proj2 .: (north_halfline a) ; :: thesis: a `2 <= r

then consider x being object such that

A2: x in the carrier of (TOP-REAL 2) and

A3: x in north_halfline a and

A4: r = proj2 . x by FUNCT_2:64;

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

r = x `2 by A4, PSCOMP_1:def 6;

hence a `2 <= r by A3, TOPREAL1:def 10; :: thesis: verum

end;assume r in proj2 .: (north_halfline a) ; :: thesis: a `2 <= r

then consider x being object such that

A2: x in the carrier of (TOP-REAL 2) and

A3: x in north_halfline a and

A4: r = proj2 . x by FUNCT_2:64;

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

r = x `2 by A4, PSCOMP_1:def 6;

hence a `2 <= r by A3, TOPREAL1:def 10; :: thesis: verum

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

ex r being Real st

( r in proj2 .: (north_halfline a) & r < (a `2) + s )

proj2 .: (north_halfline a) is bounded_below
by Th3;ex r being Real st

( r in proj2 .: (north_halfline a) & 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 .: (north_halfline a) & r < (a `2) + s ) )

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

( r in proj2 .: (north_halfline a) & r < (a `2) + s )

then A6: r + 0 < (a `2) + s by XREAL_1:8;

take r = r; :: thesis: ( r in proj2 .: (north_halfline a) & r < (a `2) + s )

( a in north_halfline a & r = proj2 . a ) by PSCOMP_1:def 6, TOPREAL1:38;

hence r in proj2 .: (north_halfline a) by FUNCT_2:35; :: thesis: r < (a `2) + s

thus r < (a `2) + s by A6; :: thesis: verum

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

( r in proj2 .: (north_halfline a) & r < (a `2) + s ) )

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

( r in proj2 .: (north_halfline a) & r < (a `2) + s )

then A6: r + 0 < (a `2) + s by XREAL_1:8;

take r = r; :: thesis: ( r in proj2 .: (north_halfline a) & r < (a `2) + s )

( a in north_halfline a & r = proj2 . a ) by PSCOMP_1:def 6, TOPREAL1:38;

hence r in proj2 .: (north_halfline a) by FUNCT_2:35; :: thesis: r < (a `2) + s

thus r < (a `2) + s by A6; :: thesis: verum

hence lower_bound (proj2 .: (north_halfline a)) = a `2 by A1, A5, SEQ_4:def 2; :: thesis: verum