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