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 set ; :: 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: (N-min X) `2 = (N-max X) `2 by Th95;
( p `2 = (N-min X) `2 & (N-min X) `1 <= p `1 & p `1 <= (N-max X) `1 ) by A1, Th98;
hence x in LSeg (N-min X),(N-max X) by A2, GOBOARD7:9; :: thesis: verum