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

now

let x be set ; :: thesis: ( ( x in (LSeg (SW-corner X),(W-min X)) /\ X implies x = W-min X ) & ( x = W-min X implies x in (LSeg (SW-corner X),(W-min X)) /\ X ) )
A1: W-min X in LSeg (SW-corner X),(W-min X) by RLTOPSP1:69;

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

W-min X in W-most X by Th91;
then ( SW-corner X in LSeg (SW-corner X),(NW-corner X) & W-min X in LSeg (SW-corner X),(NW-corner X) ) by RLTOPSP1:69, XBOOLE_0:def 4;
then A2: LSeg (SW-corner X),(W-min X) c= LSeg (SW-corner X),(NW-corner X) by TOPREAL1:12;
assume A3: x in (LSeg (SW-corner X),(W-min X)) /\ X ; :: thesis: x = W-min X
then A4: x in LSeg (SW-corner X),(W-min X) by XBOOLE_0:def 4;
reconsider p = x as Point of (TOP-REAL 2) by A3;
x in X by A3, XBOOLE_0:def 4;
then p in W-most X by A4, A2, XBOOLE_0:def 4;
then A5: (W-min X) `2 <= p `2 by Th88;
(SW-corner X) `2 <= (W-min X) `2 by Th87;
then p `2 <= (W-min X) `2 by A4, TOPREAL1:10;
then A6: p `2 = (W-min X) `2 by A5, XXREAL_0:1;
(SW-corner X) `1 = (W-min X) `1 by Th85;
then A7: p `1 = (W-min X) `1 by A4, GOBOARD7:5;
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
hence x = W-min X by A7, A6, EUCLID:57; :: thesis: verum

end;

W-min X in W-most X by Th91;
then A8: W-min X in X by XBOOLE_0:def 4;
assume x = W-min X ; :: thesis: x in (LSeg (SW-corner X),(W-min X)) /\ X
hence x in (LSeg (SW-corner X),(W-min X)) /\ X by A8, A1, XBOOLE_0:def 4; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( ( x in (LSeg (W-max X),(NW-corner X)) /\ X implies x = W-max X ) & ( x = W-max X implies x in (LSeg (W-max X),(NW-corner X)) /\ X ) )
A9: W-max X in LSeg (W-max X),(NW-corner X) by RLTOPSP1:69;

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

W-max X in W-most X by Th91;
then ( NW-corner X in LSeg (SW-corner X),(NW-corner X) & W-max X in LSeg (SW-corner X),(NW-corner X) ) by RLTOPSP1:69, XBOOLE_0:def 4;
then A10: LSeg (W-max X),(NW-corner X) c= LSeg (SW-corner X),(NW-corner X) by TOPREAL1:12;
assume A11: x in (LSeg (W-max X),(NW-corner X)) /\ X ; :: thesis: x = W-max X
then A12: x in LSeg (W-max X),(NW-corner X) by XBOOLE_0:def 4;
reconsider p = x as Point of (TOP-REAL 2) by A11;
x in X by A11, XBOOLE_0:def 4;
then p in W-most X by A12, A10, XBOOLE_0:def 4;
then A13: p `2 <= (W-max X) `2 by Th88;
(W-max X) `2 <= (NW-corner X) `2 by Th87;
then (W-max X) `2 <= p `2 by A12, TOPREAL1:10;
then A14: p `2 = (W-max X) `2 by A13, XXREAL_0:1;
(NW-corner X) `1 = (W-max X) `1 by Th85;
then A15: p `1 = (W-max X) `1 by A12, GOBOARD7:5;
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
hence x = W-max X by A15, A14, EUCLID:57; :: thesis: verum

end;

W-max X in W-most X by Th91;
then A16: W-max X in X by XBOOLE_0:def 4;
assume x = W-max X ; :: thesis: x in (LSeg (W-max X),(NW-corner X)) /\ X
hence x in (LSeg (W-max X),(NW-corner X)) /\ X by A16, A9, XBOOLE_0:def 4; :: thesis: verum

end;

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