let p, q be Point of (TOP-REAL 2); :: thesis: ( p `2 <= q `2 implies N-bound (LSeg (p,q)) = q `2 )
assume A1: p `2 <= q `2 ; :: thesis: N-bound (LSeg (p,q)) = q `2
then A2: proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).] by Th53;
thus N-bound (LSeg (p,q)) = upper_bound (proj2 .: (LSeg (p,q))) by Th45
.= q `2 by A1, A2, JORDAN5A:19 ; :: thesis: verum