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