let C be non empty compact Subset of (TOP-REAL 2); :: thesis: (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) = {(NW-corner C)}
for a being object holds
( a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) iff a = NW-corner C )

proof

let a be object ; :: thesis: ( a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) iff a = NW-corner C )
thus ( a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) implies a = NW-corner C ) :: thesis: ( a = NW-corner C implies a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) )

proof

assume A1: a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) ; :: thesis: a = NW-corner C
then a in LSeg ((NW-corner C),(NE-corner C)) by XBOOLE_0:def 4;
then 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 Th25;
then A2: 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 ) ;
a in LSeg ((SW-corner C),(NW-corner C)) by A1, XBOOLE_0:def 4;
then 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 Th26;
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 = NW-corner C by A2, EUCLID:53; :: thesis: verum

end;

assume A3: a = NW-corner C ; :: thesis: a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C)))
then A4: a in LSeg ((NW-corner C),(NE-corner C)) by RLTOPSP1:68;
a in LSeg ((SW-corner C),(NW-corner C)) by A3, RLTOPSP1:68;
hence a in (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

hence (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) = {(NW-corner C)} by TARSKI:def 1; :: thesis: verum