let a be Point of (TOP-REAL 2); :: thesis: sup (proj2 .: (south_halfline a)) = a `2
set X = proj2 .: (south_halfline a);
A1: proj2 .: (south_halfline a) is bounded_above by Th5;

A2: now

let r be real number ; :: thesis: ( r in proj2 .: (south_halfline a) implies r <= a `2 )
assume r in proj2 .: (south_halfline a) ; :: thesis: r <= a `2
then consider x being set such that
A3: x in the carrier of (TOP-REAL 2) and
A4: x in south_halfline a and
A5: r = proj2 . x by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A3;
r = x `2 by A5, PSCOMP_1:def 29;
hence r <= a `2 by A4, TOPREAL1:def 14; :: thesis: verum

end;

now

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in proj2 .: (south_halfline a) & (a `2 ) - s < r ) )
assume A6: 0 < s ; :: thesis: ex r being real number st
( r in proj2 .: (south_halfline a) & (a `2 ) - s < r )
reconsider r = a `2 as real number ;
take r = r; :: thesis: ( r in proj2 .: (south_halfline a) & (a `2 ) - s < r )
( a in south_halfline a & r = proj2 . a ) by PSCOMP_1:def 29, TOPREAL1:45;
hence r in proj2 .: (south_halfline a) by FUNCT_2:43; :: thesis: (a `2 ) - s < r
(a `2 ) - s < r - 0 by A6, XREAL_1:17;
hence (a `2 ) - s < r ; :: thesis: verum

end;

hence sup (proj2 .: (south_halfline a)) = a `2 by A1, A2, SEQ_4:def 4; :: thesis: verum