set p1X = proj1 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A13: ( (SE-corner X) `1 = E-bound X & (NE-corner X) `1 = E-bound X ) by EUCLID:52;
(proj1 | X) .: the carrier of ((TOP-REAL 2) | X) is with_max by MEASURE6:def 12;
then upper_bound ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj1 | X) .: the carrier of ((TOP-REAL 2) | X) ;
then consider p being object such that
A14: p in the carrier of ((TOP-REAL 2) | X) and
p in the carrier of ((TOP-REAL 2) | X) and
A15: upper_bound ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj1 | X) . p by FUNCT_2:64;
A16: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A14;
A17: p `2 <= N-bound X by A16, A14, Lm3;
A18: ( (SE-corner X) `2 = S-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:52;
( (proj1 | X) . p = p `1 & S-bound X <= p `2 ) by A16, A14, Lm3, Th22;
then p in LSeg ((SE-corner X),(NE-corner X)) by A13, A18, A15, A17, GOBOARD7:7;
hence ( not E-most X is empty & E-most X is compact ) by A16, A14, XBOOLE_0:def 4; :: thesis: verum