let X be non empty compact Subset of (TOP-REAL 2); :: thesis: ( (LSeg (SE-corner X),(E-min X)) /\ X = {(E-min X)} & (LSeg (E-max X),(NE-corner X)) /\ X = {(E-max X)} )
now let x be
set ;
:: thesis: ( ( 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 ) )hereby :: thesis: ( x = E-min X implies x in (LSeg (SE-corner X),(E-min X)) /\ X )
assume A1:
x in (LSeg (SE-corner X),(E-min X)) /\ X
;
:: thesis: x = E-min Xthen A2:
(
x in LSeg (SE-corner X),
(E-min X) &
x in X )
by XBOOLE_0:def 4;
reconsider p =
x as
Point of
(TOP-REAL 2) by A1;
(SE-corner X) `1 = (E-min X) `1
by Th105;
then A3:
p `1 = (E-min X) `1
by A2, GOBOARD7:5;
(SE-corner X) `2 <= (E-min X) `2
by Th107;
then A4:
p `2 <= (E-min X) `2
by A2, TOPREAL1:10;
A5:
SE-corner X in LSeg (SE-corner X),
(NE-corner X)
by RLTOPSP1:69;
E-min X in E-most X
by Th111;
then
E-min X in LSeg (SE-corner X),
(NE-corner X)
by XBOOLE_0:def 4;
then
LSeg (SE-corner X),
(E-min X) c= LSeg (SE-corner X),
(NE-corner X)
by A5, TOPREAL1:12;
then
p in E-most X
by A2, XBOOLE_0:def 4;
then
(E-min X) `2 <= p `2
by Th108;
then A6:
p `2 = (E-min X) `2
by A4, XXREAL_0:1;
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
hence
x = E-min X
by A3, A6, EUCLID:57;
:: thesis: verum
end; assume A7:
x = E-min X
;
:: thesis: x in (LSeg (SE-corner X),(E-min X)) /\ X
E-min X in E-most X
by Th111;
then A8:
E-min X in X
by XBOOLE_0:def 4;
E-min X in LSeg (SE-corner X),
(E-min X)
by RLTOPSP1:69;
hence
x in (LSeg (SE-corner X),(E-min X)) /\ X
by A7, A8, XBOOLE_0:def 4;
:: thesis: verum end;
hence
(LSeg (SE-corner X),(E-min X)) /\ X = {(E-min X)}
by TARSKI:def 1; :: thesis: (LSeg (E-max X),(NE-corner X)) /\ X = {(E-max X)}
now let x be
set ;
:: thesis: ( ( 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 ) )hereby :: thesis: ( x = E-max X implies x in (LSeg (E-max X),(NE-corner X)) /\ X )
assume A9:
x in (LSeg (E-max X),(NE-corner X)) /\ X
;
:: thesis: x = E-max Xthen A10:
(
x in LSeg (E-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) `1 = (E-max X) `1
by Th105;
then A11:
p `1 = (E-max X) `1
by A10, GOBOARD7:5;
(E-max X) `2 <= (NE-corner X) `2
by Th107;
then A12:
(E-max X) `2 <= p `2
by A10, TOPREAL1:10;
A13:
NE-corner X in LSeg (SE-corner X),
(NE-corner X)
by RLTOPSP1:69;
E-max X in E-most X
by Th111;
then
E-max X in LSeg (SE-corner X),
(NE-corner X)
by XBOOLE_0:def 4;
then
LSeg (E-max X),
(NE-corner X) c= LSeg (SE-corner X),
(NE-corner X)
by A13, TOPREAL1:12;
then
p in E-most X
by A10, XBOOLE_0:def 4;
then
p `2 <= (E-max X) `2
by Th108;
then A14:
p `2 = (E-max X) `2
by A12, XXREAL_0:1;
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
hence
x = E-max X
by A11, A14, EUCLID:57;
:: thesis: verum
end; assume A15:
x = E-max X
;
:: thesis: x in (LSeg (E-max X),(NE-corner X)) /\ X
E-max X in E-most X
by Th111;
then A16:
E-max X in X
by XBOOLE_0:def 4;
E-max X in LSeg (E-max X),
(NE-corner X)
by RLTOPSP1:69;
hence
x in (LSeg (E-max X),(NE-corner X)) /\ X
by A15, A16, XBOOLE_0:def 4;
:: thesis: verum end;
hence
(LSeg (E-max X),(NE-corner X)) /\ X = {(E-max X)}
by TARSKI:def 1; :: thesis: verum