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