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:56;
(proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X)) is left_end
by MEASURE6:def 17;
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))
by MEASURE6:def 9;
then consider p being set 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:115;
A4:
the carrier of ((TOP-REAL 2) | (E-most X)) = E-most X
by PRE_TOPC:29;
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:56;
(proj2 | (E-most X)) . p = p `2
by A4, A2, Th70;
hence
E-min X in E-most X
by A4, A2, A3, A5, EUCLID:57; E-max X in E-most X
(proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X)) is right_end
by MEASURE6:def 16;
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))
by MEASURE6:def 8;
then consider p being set 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:115;
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, Th70;
hence
E-max X in E-most X
by A4, A7, A8, A9, EUCLID:57; verum