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