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