let X be compact Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in X & p `2 = N-bound X holds
p in N-most X
let p be Point of (TOP-REAL 2); :: thesis: ( p in X & p `2 = N-bound X implies p in N-most X )
assume that
A1: p in X and
A2: p `2 = N-bound X ; :: thesis: p in N-most X
A3: ( (NW-corner X) `2 = N-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:52;
A4: ( (NW-corner X) `1 = W-bound X & (NE-corner X) `1 = E-bound X ) by EUCLID:52;
( W-bound X <= p `1 & p `1 <= E-bound X ) by A1, PSCOMP_1:24;
then p in LSeg ((NW-corner X),(NE-corner X)) by A2, A3, A4, GOBOARD7:8;
hence p in N-most X by A1, XBOOLE_0:def 4; :: thesis: verum