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