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