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 Th61;
thus S-bound (LSeg p,q) = inf (proj2 .: (LSeg p,q)) by Th49
.= p `2 by A1, A2, JORDAN5A:20 ; :: thesis: verum