let a be Point of (TOP-REAL 2); :: thesis: proj1 .: (east_halfline a) is bounded_below
take a `1 ; :: according to XXREAL_2:def 9 :: thesis: a `1 is LowerBound of proj1 .: (east_halfline a)
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in proj1 .: (east_halfline a) or a `1 <= r )
assume r in proj1 .: (east_halfline a) ; :: thesis: a `1 <= r
then consider x being object such that
A1: x in the carrier of (TOP-REAL 2) and
A2: x in east_halfline a and
A3: r = proj1 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A1;
r = x `1 by A3, PSCOMP_1:def 5;
hence a `1 <= r by A2, TOPREAL1:def 11; :: thesis: verum