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