let C be non empty compact Subset of (TOP-REAL 2); 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
by EUCLID:52;
A2:
(SW-corner C) `2 = S-bound C
by EUCLID:52;
A3:
(NW-corner C) `1 = W-bound C
by EUCLID:52;
A4:
(NW-corner C) `2 = N-bound C
by EUCLID:52;
A5:
S-bound C <= N-bound C
by Th22;
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 ) }
XBOOLE_0:def 10 { 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
object ;
TARSKI:def 3 ( 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 A6:
a in LSeg (
(SW-corner C),
(NW-corner C))
;
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) ;
A7:
p `1 = W-bound C
by A1, A3, A6, GOBOARD7:5;
A8:
p `2 >= S-bound C
by A2, A4, A5, A6, TOPREAL1:4;
p `2 <= N-bound C
by A2, A4, A5, A6, TOPREAL1:4;
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 A7, A8;
verum
end;
let a be object ; TARSKI:def 3 ( 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 ) }
; 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, A3, A4, GOBOARD7:7; verum