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