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 :: thesis: for x being object holds
( ( 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 ) )

let x be object ; :: 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 ) )
A1: N-min X in LSeg ((NW-corner X),(N-min X)) by RLTOPSP1:68;

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

N-min X in N-most X by Th42;
then ( NW-corner X in LSeg ((NW-corner X),(NE-corner X)) & N-min X in LSeg ((NW-corner X),(NE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def 4;
then A2: LSeg ((NW-corner X),(N-min X)) c= LSeg ((NW-corner X),(NE-corner X)) by TOPREAL1:6;
assume A3: x in (LSeg ((NW-corner X),(N-min X))) /\ X ; :: thesis: x = N-min X
then A4: x in LSeg ((NW-corner X),(N-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 N-most X by A4, A2, XBOOLE_0:def 4;
then A5: (N-min X) `1 <= p `1 by Th39;
(NW-corner X) `1 <= (N-min X) `1 by Th38;
then p `1 <= (N-min X) `1 by A4, TOPREAL1:3;
then A6: p `1 = (N-min X) `1 by A5, XXREAL_0:1;
(NW-corner X) `2 = (N-min X) `2 by Th37;
then A7: p `2 = (N-min X) `2 by A4, GOBOARD7:6;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = N-min X by A7, A6, EUCLID:53; :: thesis: verum

end;

N-min X in N-most X by Th42;
then A8: N-min X in X by XBOOLE_0:def 4;
assume x = N-min X ; :: thesis: x in (LSeg ((NW-corner X),(N-min X))) /\ X
hence x in (LSeg ((NW-corner X),(N-min X))) /\ X by A8, A1, 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 :: thesis: for x being object holds
( ( 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 ) )

let x be object ; :: 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 ) )
A9: N-max X in LSeg ((N-max X),(NE-corner X)) by RLTOPSP1:68;

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

N-max X in N-most X by Th42;
then ( NE-corner X in LSeg ((NW-corner X),(NE-corner X)) & N-max X in LSeg ((NW-corner X),(NE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def 4;
then A10: LSeg ((N-max X),(NE-corner X)) c= LSeg ((NW-corner X),(NE-corner X)) by TOPREAL1:6;
assume A11: x in (LSeg ((N-max X),(NE-corner X))) /\ X ; :: thesis: x = N-max X
then A12: x in LSeg ((N-max X),(NE-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 N-most X by A12, A10, XBOOLE_0:def 4;
then A13: p `1 <= (N-max X) `1 by Th39;
(N-max X) `1 <= (NE-corner X) `1 by Th38;
then (N-max X) `1 <= p `1 by A12, TOPREAL1:3;
then A14: p `1 = (N-max X) `1 by A13, XXREAL_0:1;
(NE-corner X) `2 = (N-max X) `2 by Th37;
then A15: p `2 = (N-max X) `2 by A12, GOBOARD7:6;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = N-max X by A15, A14, EUCLID:53; :: thesis: verum

end;

N-max X in N-most X by Th42;
then A16: N-max X in X by XBOOLE_0:def 4;
assume x = N-max X ; :: thesis: x in (LSeg ((N-max X),(NE-corner X))) /\ X
hence x in (LSeg ((N-max X),(NE-corner X))) /\ X by A16, A9, 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