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