let X be non empty compact Subset of (TOP-REAL 2); ( (LSeg ((SE-corner X),(E-min X))) /\ X = {(E-min X)} & (LSeg ((E-max X),(NE-corner X))) /\ X = {(E-max X)} )
now for x being object holds
( ( x in (LSeg ((SE-corner X),(E-min X))) /\ X implies x = E-min X ) & ( x = E-min X implies x in (LSeg ((SE-corner X),(E-min X))) /\ X ) )let x be
object ;
( ( x in (LSeg ((SE-corner X),(E-min X))) /\ X implies x = E-min X ) & ( x = E-min X implies x in (LSeg ((SE-corner X),(E-min X))) /\ X ) )A1:
E-min X in LSeg (
(SE-corner X),
(E-min X))
by RLTOPSP1:68;
hereby ( x = E-min X implies x in (LSeg ((SE-corner X),(E-min X))) /\ X )
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
;
x = E-min Xthen 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;
verum
end;
E-min X in E-most X
by Th50;
then A8:
E-min X in X
by XBOOLE_0:def 4;
assume
x = E-min X
;
x in (LSeg ((SE-corner X),(E-min X))) /\ Xhence
x in (LSeg ((SE-corner X),(E-min X))) /\ X
by A8, A1, XBOOLE_0:def 4;
verum end;
hence
(LSeg ((SE-corner X),(E-min X))) /\ X = {(E-min X)}
by TARSKI:def 1; (LSeg ((E-max X),(NE-corner X))) /\ X = {(E-max X)}
now for x being object holds
( ( x in (LSeg ((E-max X),(NE-corner X))) /\ X implies x = E-max X ) & ( x = E-max X implies x in (LSeg ((E-max X),(NE-corner X))) /\ X ) )let x be
object ;
( ( x in (LSeg ((E-max X),(NE-corner X))) /\ X implies x = E-max X ) & ( x = E-max X implies x in (LSeg ((E-max X),(NE-corner X))) /\ X ) )A9:
E-max X in LSeg (
(E-max X),
(NE-corner X))
by RLTOPSP1:68;
hereby ( x = E-max X implies x in (LSeg ((E-max X),(NE-corner X))) /\ X )
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
;
x = E-max Xthen 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;
verum
end;
E-max X in E-most X
by Th50;
then A16:
E-max X in X
by XBOOLE_0:def 4;
assume
x = E-max X
;
x in (LSeg ((E-max X),(NE-corner X))) /\ Xhence
x in (LSeg ((E-max X),(NE-corner X))) /\ X
by A16, A9, XBOOLE_0:def 4;
verum end;
hence
(LSeg ((E-max X),(NE-corner X))) /\ X = {(E-max X)}
by TARSKI:def 1; verum