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