E-min X in E-most X by Th50;
then ( SE-corner X in LSeg ((SE-corner X),(NE-corner X)) & E-min X in LSeg ((SE-corner X),(NE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def 4;
then A2: LSeg ((SE-corner X),(E-min X)) c= LSeg ((SE-corner X),(NE-corner X)) by TOPREAL1:6;
assume A3: x in (LSeg ((SE-corner X),(E-min X))) /\ X ; :: thesis: x = E-min X
then A4: x in LSeg ((SE-corner X),(E-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 E-most X by A4, A2, XBOOLE_0:def 4;
then A5: (E-min X) `2 <= p `2 by Th47;
(SE-corner X) `2 <= (E-min X) `2 by Th46;
then p `2 <= (E-min X) `2 by A4, TOPREAL1:4;
then A6: p `2 = (E-min X) `2 by A5, XXREAL_0:1;
(SE-corner X) `1 = (E-min X) `1 by Th45;
then A7: p `1 = (E-min X) `1 by A4, GOBOARD7:5;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = E-min X by A7, A6, EUCLID:53; :: thesis: verum

E-max X in E-most X by Th50;
then ( NE-corner X in LSeg ((SE-corner X),(NE-corner X)) & E-max X in LSeg ((SE-corner X),(NE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def 4;
then A10: LSeg ((E-max X),(NE-corner X)) c= LSeg ((SE-corner X),(NE-corner X)) by TOPREAL1:6;
assume A11: x in (LSeg ((E-max X),(NE-corner X))) /\ X ; :: thesis: x = E-max X
then A12: x in LSeg ((E-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 E-most X by A12, A10, XBOOLE_0:def 4;
then A13: p `2 <= (E-max X) `2 by Th47;
(E-max X) `2 <= (NE-corner X) `2 by Th46;
then (E-max X) `2 <= p `2 by A12, TOPREAL1:4;
then A14: p `2 = (E-max X) `2 by A13, XXREAL_0:1;
(NE-corner X) `1 = (E-max X) `1 by Th45;
then A15: p `1 = (E-max X) `1 by A12, GOBOARD7:5;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = E-max X by A15, A14, EUCLID:53; :: thesis: verum