set p2X = proj2 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A7: ( (NW-corner X) `1 = W-bound X & (NE-corner X) `1 = E-bound X ) by EUCLID:56;
(proj2 | X) .: the carrier of ((TOP-REAL 2) | X) is with_max by Def14;
then sup ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj2 | X) .: the carrier of ((TOP-REAL 2) | X) by Def3;
then consider p being set such that
A8: p in the carrier of ((TOP-REAL 2) | X) and
p in the carrier of ((TOP-REAL 2) | X) and
A9: sup ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj2 | X) . p by FUNCT_2:115;
A10: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:29;
then reconsider p = p as Point of (TOP-REAL 2) by A8;
A11: p `1 <= E-bound X by A10, A8, Lm9;
A12: ( (NW-corner X) `2 = N-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:56;
( (proj2 | X) . p = p `2 & W-bound X <= p `1 ) by A10, A8, Lm9, Th70;
then p in LSeg (NW-corner X),(NE-corner X) by A7, A12, A9, A11, GOBOARD7:9;
hence ( not N-most X is empty & N-most X is compact ) by A10, A8, Th64, XBOOLE_0:def 4; :: thesis: verum