let p be Point of (TOP-REAL 2); :: thesis: for Z being non empty Subset of (TOP-REAL 2) st p in W-most Z holds
( p `1 = (W-min Z) `1 & ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) ) )
let Z be non empty Subset of (TOP-REAL 2); :: thesis: ( p in W-most Z implies ( p `1 = (W-min Z) `1 & ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) ) ) )
A1: ( (SW-corner Z) `1 = W-bound Z & (W-min Z) `1 = W-bound Z ) by EUCLID:52;
A2: (NW-corner Z) `1 = W-bound Z by EUCLID:52;
assume A3: p in W-most Z ; :: thesis: ( p `1 = (W-min Z) `1 & ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) ) )
then p in LSeg ((SW-corner Z),(NW-corner Z)) by XBOOLE_0:def 4;
hence p `1 = (W-min Z) `1 by A1, A2, GOBOARD7:5; :: thesis: ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) )
assume Z is compact ; :: thesis: ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 )
then reconsider Z = Z as non empty compact Subset of (TOP-REAL 2) ;
( (W-min Z) `2 = lower_bound (proj2 | (W-most Z)) & (W-max Z) `2 = upper_bound (proj2 | (W-most Z)) ) by EUCLID:52;
hence ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) by A3, Lm3; :: thesis: verum