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 object ; :: 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, Th47;
A3: (E-min X) `1 = (E-max X) `1 by Th45;
( p `1 = (E-min X) `1 & (E-min X) `2 <= p `2 ) by A1, Th47;
hence x in LSeg ((E-min X),(E-max X)) by A3, A2, GOBOARD7:7; :: thesis: verum