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

proof

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

proof

assume A1: a in (LSeg (NW-corner C),(NE-corner C)) /\ (LSeg (NE-corner C),(SE-corner C)) ; :: thesis: a = NE-corner C
then a in LSeg (NE-corner C),(SE-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 `2 <= N-bound C & p `2 >= S-bound C ) } by Th25;
then A2: 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 ) ;
a in LSeg (NW-corner C),(NE-corner C) by A1, 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 Th27;
then 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 ) ;
hence a = NE-corner C by A2, EUCLID:57; :: thesis: verum

end;

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

end;

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