let X be non empty compact Subset of (TOP-REAL 2); :: thesis: ( 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: the carrier of ((TOP-REAL 2) | (S-most X)) = S-most X by PRE_TOPC:29;
(proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X)) is with_min by Def15;
then inf ((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)) by Def4;
then consider p being set such that
A2: ( p in the carrier of ((TOP-REAL 2) | (S-most X)) & p in the carrier of ((TOP-REAL 2) | (S-most X)) & inf ((proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X))) = (proj1 | (S-most X)) . p ) by FUNCT_2:115;
reconsider p = p as Point of (TOP-REAL 2) by A1, A2;
A3: (proj1 | (S-most X)) . p = p `1 by A1, A2, Th69;
A4: p in LSeg (SW-corner X),(SE-corner X) by A1, A2, XBOOLE_0:def 4;
( (SW-corner X) `2 = S-bound X & (SE-corner X) `2 = S-bound X ) by EUCLID:56;
then p `2 = S-bound X by A4, GOBOARD7:6;
hence S-min X in S-most X by A1, A2, A3, EUCLID:57; :: thesis: S-max X in S-most X
(proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X)) is with_max by Def14;
then sup ((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)) by Def3;
then consider p being set such that
A5: ( p in the carrier of ((TOP-REAL 2) | (S-most X)) & p in the carrier of ((TOP-REAL 2) | (S-most X)) & sup ((proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X))) = (proj1 | (S-most X)) . p ) by FUNCT_2:115;
reconsider p = p as Point of (TOP-REAL 2) by A1, A5;
A6: (proj1 | (S-most X)) . p = p `1 by A1, A5, Th69;
A7: p in LSeg (SW-corner X),(SE-corner X) by A1, A5, XBOOLE_0:def 4;
( (SW-corner X) `2 = S-bound X & (SE-corner X) `2 = S-bound X ) by EUCLID:56;
then p `2 = S-bound X by A7, GOBOARD7:6;
hence S-max X in S-most X by A1, A5, A6, EUCLID:57; :: thesis: verum