let a be Point of (TOP-REAL 2); :: thesis: proj2 .: (north_halfline a) is bounded_below

take a `2 ; :: according to XXREAL_2:def 9 :: thesis: a `2 is LowerBound of proj2 .: (north_halfline a)

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in proj2 .: (north_halfline a) or a `2 <= r )

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

then consider x being object such that

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

A2: x in north_halfline a and

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

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

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

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

take a `2 ; :: according to XXREAL_2:def 9 :: thesis: a `2 is LowerBound of proj2 .: (north_halfline a)

let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in proj2 .: (north_halfline a) or a `2 <= r )

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

then consider x being object such that

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

A2: x in north_halfline a and

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

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

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

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