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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg (SW-corner C),(NW-corner C) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) } )
assume A4: a in LSeg (SW-corner C),(NW-corner C) ; :: thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) }
then reconsider p = a as Point of (TOP-REAL 2) ;
A5: p `1 = W-bound C by A1, A2, A4, GOBOARD7:5;
( p `2 <= N-bound C & p `2 >= S-bound C ) by A1, A2, A3, A4, TOPREAL1:10;
hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) } by A5; :: 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 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) } or a in LSeg (SW-corner C),(NW-corner C) )
assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) } ; :: thesis: a in LSeg (SW-corner C),(NW-corner C)
then ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = W-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) ;
hence a in LSeg (SW-corner C),(NW-corner C) by A1, A2, GOBOARD7:8; :: thesis: verum