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