let X be non empty compact Subset of (TOP-REAL 2); :: thesis: E-most X c= LSeg (E-min X),(E-max X)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in E-most X or x in LSeg (E-min X),(E-max X) )
assume A1: x in E-most X ; :: thesis: x in LSeg (E-min X),(E-max X)
then reconsider p = x as Point of (TOP-REAL 2) ;
A2: p `2 <= (E-max X) `2 by A1, Th108;
A3: (E-min X) `1 = (E-max X) `1 by Th105;
( p `1 = (E-min X) `1 & (E-min X) `2 <= p `2 ) by A1, Th108;
hence x in LSeg (E-min X),(E-max X) by A3, A2, GOBOARD7:8; :: thesis: verum