let D be non empty Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in S-most D holds
p `2 = S-bound D
let p be Point of (TOP-REAL 2); :: thesis: ( p in S-most D implies p `2 = S-bound D )
assume p in S-most D ; :: thesis: p `2 = S-bound D
then A1: p in LSeg ((SW-corner D),(SE-corner D)) by XBOOLE_0:def 4;
(SE-corner D) `2 = S-bound D by EUCLID:52
.= (SW-corner D) `2 by EUCLID:52 ;
hence p `2 = (SW-corner D) `2 by A1, GOBOARD7:6
.= S-bound D by EUCLID:52 ;
:: thesis: verum