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:52;
(proj2 | X) .: the carrier of ((TOP-REAL 2) | X) is with_max
by MEASURE6:def 12;
then
upper_bound ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj2 | X) .: the carrier of ((TOP-REAL 2) | X)
;
then consider p being object such that
A8:
p in the carrier of ((TOP-REAL 2) | X)
and
p in the carrier of ((TOP-REAL 2) | X)
and
A9:
upper_bound ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj2 | X) . p
by FUNCT_2:64;
A10:
the carrier of ((TOP-REAL 2) | X) = X
by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A8;
A11:
p `1 <= E-bound X
by A10, A8, Lm3;
A12:
( (NW-corner X) `2 = N-bound X & (NE-corner X) `2 = N-bound X )
by EUCLID:52;
( (proj2 | X) . p = p `2 & W-bound X <= p `1 )
by A10, A8, Lm3, Th23;
then
p in LSeg ((NW-corner X),(NE-corner X))
by A7, A12, A9, A11, GOBOARD7:8;
hence
( not N-most X is empty & N-most X is compact )
by A10, A8, XBOOLE_0:def 4; verum