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

A1: now :: thesis: for r being Real st r in proj1 .: (east_halfline a) holds
a `1 <= r

let r be Real; :: thesis: ( r in proj1 .: (east_halfline a) implies a `1 <= r )
assume r in proj1 .: (east_halfline a) ; :: thesis: a `1 <= r
then consider x being object such that
A2: x in the carrier of (TOP-REAL 2) and
A3: x in east_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 a `1 <= r by A3, TOPREAL1:def 11; :: thesis: verum

end;

A5: now :: thesis: for s being Real st 0 < s holds
ex r being Real st
( r in proj1 .: (east_halfline a) & r < (a `1) + s )

reconsider r = a `1 as Real ;
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in proj1 .: (east_halfline a) & r < (a `1) + s ) )
assume 0 < s ; :: thesis: ex r being Real st
( r in proj1 .: (east_halfline a) & r < (a `1) + s )
then A6: r + 0 < (a `1) + s by XREAL_1:8;
take r = r; :: thesis: ( r in proj1 .: (east_halfline a) & r < (a `1) + s )
( a in east_halfline a & r = proj1 . a ) by PSCOMP_1:def 5, TOPREAL1:38;
hence r in proj1 .: (east_halfline a) by FUNCT_2:35; :: thesis: r < (a `1) + s
thus r < (a `1) + s by A6; :: thesis: verum

end;

proj1 .: (east_halfline a) is bounded_below by Th6;
hence lower_bound (proj1 .: (east_halfline a)) = a `1 by A1, A5, SEQ_4:def 2; :: thesis: verum