let X be non empty compact Subset of (TOP-REAL 2); :: thesis: ( (LSeg (NW-corner X),(N-min X)) /\ X = {(N-min X)} & (LSeg (N-max X),(NE-corner X)) /\ X = {(N-max X)} )

now

let x be set ; :: thesis: ( ( x in (LSeg (NW-corner X),(N-min X)) /\ X implies x = N-min X ) & ( x = N-min X implies x in (LSeg (NW-corner X),(N-min X)) /\ X ) )

hereby :: thesis: ( x = N-min X implies x in (LSeg (NW-corner X),(N-min X)) /\ X )

assume A1: x in (LSeg (NW-corner X),(N-min X)) /\ X ; :: thesis: x = N-min X
then A2: ( x in LSeg (NW-corner X),(N-min X) & x in X ) by XBOOLE_0:def 4;
reconsider p = x as Point of (TOP-REAL 2) by A1;
(NW-corner X) `2 = (N-min X) `2 by Th95;
then A3: p `2 = (N-min X) `2 by A2, GOBOARD7:6;
(NW-corner X) `1 <= (N-min X) `1 by Th97;
then A4: p `1 <= (N-min X) `1 by A2, TOPREAL1:9;
A5: NW-corner X in LSeg (NW-corner X),(NE-corner X) by RLTOPSP1:69;
N-min X in N-most X by Th101;
then N-min X in LSeg (NW-corner X),(NE-corner X) by XBOOLE_0:def 4;
then LSeg (NW-corner X),(N-min X) c= LSeg (NW-corner X),(NE-corner X) by A5, TOPREAL1:12;
then p in N-most X by A2, XBOOLE_0:def 4;
then (N-min X) `1 <= p `1 by Th98;
then A6: p `1 = (N-min X) `1 by A4, XXREAL_0:1;
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
hence x = N-min X by A3, A6, EUCLID:57; :: thesis: verum

end;

assume A7: x = N-min X ; :: thesis: x in (LSeg (NW-corner X),(N-min X)) /\ X
N-min X in N-most X by Th101;
then A8: N-min X in X by XBOOLE_0:def 4;
N-min X in LSeg (NW-corner X),(N-min X) by RLTOPSP1:69;
hence x in (LSeg (NW-corner X),(N-min X)) /\ X by A7, A8, XBOOLE_0:def 4; :: thesis: verum

end;

hence (LSeg (NW-corner X),(N-min X)) /\ X = {(N-min X)} by TARSKI:def 1; :: thesis: (LSeg (N-max X),(NE-corner X)) /\ X = {(N-max X)}

now

let x be set ; :: thesis: ( ( x in (LSeg (N-max X),(NE-corner X)) /\ X implies x = N-max X ) & ( x = N-max X implies x in (LSeg (N-max X),(NE-corner X)) /\ X ) )

hereby :: thesis: ( x = N-max X implies x in (LSeg (N-max X),(NE-corner X)) /\ X )

assume A9: x in (LSeg (N-max X),(NE-corner X)) /\ X ; :: thesis: x = N-max X
then A10: ( x in LSeg (N-max X),(NE-corner X) & x in X ) by XBOOLE_0:def 4;
reconsider p = x as Point of (TOP-REAL 2) by A9;
(NE-corner X) `2 = (N-max X) `2 by Th95;
then A11: p `2 = (N-max X) `2 by A10, GOBOARD7:6;
(N-max X) `1 <= (NE-corner X) `1 by Th97;
then A12: (N-max X) `1 <= p `1 by A10, TOPREAL1:9;
A13: NE-corner X in LSeg (NW-corner X),(NE-corner X) by RLTOPSP1:69;
N-max X in N-most X by Th101;
then N-max X in LSeg (NW-corner X),(NE-corner X) by XBOOLE_0:def 4;
then LSeg (N-max X),(NE-corner X) c= LSeg (NW-corner X),(NE-corner X) by A13, TOPREAL1:12;
then p in N-most X by A10, XBOOLE_0:def 4;
then p `1 <= (N-max X) `1 by Th98;
then A14: p `1 = (N-max X) `1 by A12, XXREAL_0:1;
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
hence x = N-max X by A11, A14, EUCLID:57; :: thesis: verum

end;

assume A15: x = N-max X ; :: thesis: x in (LSeg (N-max X),(NE-corner X)) /\ X
N-max X in N-most X by Th101;
then A16: N-max X in X by XBOOLE_0:def 4;
N-max X in LSeg (N-max X),(NE-corner X) by RLTOPSP1:69;
hence x in (LSeg (N-max X),(NE-corner X)) /\ X by A15, A16, XBOOLE_0:def 4; :: thesis: verum

end;

hence (LSeg (N-max X),(NE-corner X)) /\ X = {(N-max X)} by TARSKI:def 1; :: thesis: verum