let a be Point of (TOP-REAL 2); :: thesis: inf (proj1 .: (east_halfline a)) = a `1
set X = proj1 .: (east_halfline a);
A1: proj1 .: (east_halfline a) is bounded_below by Th7;

A2: now

let r be real number ; :: 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 set such that
A3: x in the carrier of (TOP-REAL 2) and
A4: x in east_halfline a and
A5: r = proj1 . x by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A3;
r = x `1 by A5, PSCOMP_1:def 28;
hence a `1 <= r by A4, TOPREAL1:def 13; :: thesis: verum

end;

now

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in proj1 .: (east_halfline a) & r < (a `1 ) + s ) )
assume A6: 0 < s ; :: thesis: ex r being real number st
( r in proj1 .: (east_halfline a) & r < (a `1 ) + s )
reconsider r = a `1 as real number ;
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 28, TOPREAL1:45;
hence r in proj1 .: (east_halfline a) by FUNCT_2:43; :: thesis: r < (a `1 ) + s
r + 0 < (a `1 ) + s by A6, XREAL_1:10;
hence r < (a `1 ) + s ; :: thesis: verum

end;

hence inf (proj1 .: (east_halfline a)) = a `1 by A1, A2, SEQ_4:def 5; :: thesis: verum