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