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

proof

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

end;

let a be object ; :: 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 = S-bound C ) } or a in LSeg ((SW-corner C),(SE-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 = S-bound C ) } ; :: thesis: a in LSeg ((SW-corner C),(SE-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 = S-bound C ) ;
hence a in LSeg ((SW-corner C),(SE-corner C)) by A1, A3, A4, A2, GOBOARD7:8; :: thesis: verum