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