let X be non empty compact Subset of (TOP-REAL 2); ( E-min X in E-most X & E-max X in E-most X )
set p2W = proj2 | (E-most X);
set c = the carrier of ((TOP-REAL 2) | (E-most X));
A1:
( (SE-corner X) `1 = E-bound X & (NE-corner X) `1 = E-bound X )
by EUCLID:52;
(proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X)) is with_min
by MEASURE6:def 13;
then
lower_bound ((proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))) in (proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))
;
then consider p being object such that
A2:
p in the carrier of ((TOP-REAL 2) | (E-most X))
and
p in the carrier of ((TOP-REAL 2) | (E-most X))
and
A3:
lower_bound ((proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))) = (proj2 | (E-most X)) . p
by FUNCT_2:64;
A4:
the carrier of ((TOP-REAL 2) | (E-most X)) = E-most X
by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A2;
p in LSeg ((SE-corner X),(NE-corner X))
by A4, A2, XBOOLE_0:def 4;
then A5:
p `1 = E-bound X
by A1, GOBOARD7:5;
A6:
( (SE-corner X) `1 = E-bound X & (NE-corner X) `1 = E-bound X )
by EUCLID:52;
(proj2 | (E-most X)) . p = p `2
by A4, A2, Th23;
hence
E-min X in E-most X
by A4, A2, A3, A5, EUCLID:53; E-max X in E-most X
(proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X)) is with_max
by MEASURE6:def 12;
then
upper_bound ((proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))) in (proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))
;
then consider p being object such that
A7:
p in the carrier of ((TOP-REAL 2) | (E-most X))
and
p in the carrier of ((TOP-REAL 2) | (E-most X))
and
A8:
upper_bound ((proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))) = (proj2 | (E-most X)) . p
by FUNCT_2:64;
reconsider p = p as Point of (TOP-REAL 2) by A4, A7;
p in LSeg ((SE-corner X),(NE-corner X))
by A4, A7, XBOOLE_0:def 4;
then A9:
p `1 = E-bound X
by A6, GOBOARD7:5;
(proj2 | (E-most X)) . p = p `2
by A4, A7, Th23;
hence
E-max X in E-most X
by A4, A7, A8, A9, EUCLID:53; verum