let a be Point of (TOP-REAL 2); :: thesis: proj2 .: (south_halfline a) is bounded_above
take a `2 ; :: according to XXREAL_2:def 10 :: thesis: a `2 is UpperBound of proj2 .: (south_halfline a)
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in proj2 .: (south_halfline a) or r <= a `2 )
assume r in proj2 .: (south_halfline a) ; :: thesis: r <= a `2
then consider x being object such that
A1: x in the carrier of (TOP-REAL 2) and
A2: x in south_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 r <= a `2 by A2, TOPREAL1:def 12; :: thesis: verum