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