let C be non empty compact Subset of (TOP-REAL 2); :: thesis: LSeg (NW-corner C),(NE-corner C) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) }
set L = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) } ;
set q1 = NW-corner C;
set q2 = NE-corner C;
A1: (NW-corner C) `1 = W-bound C by EUCLID:56;
A2: (NE-corner C) `2 = N-bound C by EUCLID:56;
A3: (NW-corner C) `2 = N-bound C by EUCLID:56;
A4: (NE-corner C) `1 = E-bound C by EUCLID:56;
A5: W-bound C <= E-bound C by Th23;
thus LSeg (NW-corner C),(NE-corner C) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) } :: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) } c= LSeg (NW-corner C),(NE-corner C)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg (NW-corner C),(NE-corner C) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) } )
assume A6: a in LSeg (NW-corner C),(NE-corner C) ; :: thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) }
then reconsider p = a as Point of (TOP-REAL 2) ;
A7: p `2 = N-bound C by A3, A2, A6, GOBOARD7:6;
A8: p `1 >= W-bound C by A1, A4, A5, A6, TOPREAL1:9;
p `1 <= E-bound C by A1, A4, A5, A6, TOPREAL1:9;
hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) } by A7, A8; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) } or a in LSeg (NW-corner C),(NE-corner C) )
assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) } ; :: thesis: a in LSeg (NW-corner C),(NE-corner C)
then ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= E-bound C & p `1 >= W-bound C & p `2 = N-bound C ) ;
hence a in LSeg (NW-corner C),(NE-corner C) by A1, A3, A4, A2, GOBOARD7:9; :: thesis: verum