let C be non empty compact Subset of (TOP-REAL 2); :: thesis: LSeg (SE-corner C),(NE-corner C) = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-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 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) } ;
set q1 = SE-corner C;
set q2 = NE-corner C;
A1: (SE-corner C) `1 = E-bound C by EUCLID:56;
A2: (SE-corner C) `2 = S-bound C by EUCLID:56;
A3: (NE-corner C) `1 = E-bound C by EUCLID:56;
A4: (NE-corner C) `2 = N-bound C by EUCLID:56;
A5: S-bound C <= N-bound C by Th24;
thus LSeg (SE-corner C),(NE-corner C) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = E-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 = E-bound C & p `2 <= N-bound C & p `2 >= S-bound C ) } c= LSeg (SE-corner C),(NE-corner C)

proof

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