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