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