A13: ( (SW-corner X) `1 = W-bound X & (SE-corner X) `1 = E-bound X & (SW-corner X) `2 = S-bound X & (SE-corner X) `2 = S-bound X ) by EUCLID:56;
set p2X = proj2 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A14: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:29;
(proj2 | X) .: the carrier of ((TOP-REAL 2) | X) is with_min by Def15;
then inf ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj2 | X) .: the carrier of ((TOP-REAL 2) | X) by Def4;
then consider p being set such that
A15: ( p in the carrier of ((TOP-REAL 2) | X) & p in the carrier of ((TOP-REAL 2) | X) & inf ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj2 | X) . p ) by FUNCT_2:115;
reconsider p = p as Point of (TOP-REAL 2) by A14, A15;
A16: (proj2 | X) . p = p `2 by A14, A15, Th70;
( W-bound X <= p `1 & p `1 <= E-bound X ) by A14, A15, Lm9;
then p in LSeg (SW-corner X),(SE-corner X) by A13, A15, A16, GOBOARD7:9;
hence ( not S-most X is empty & S-most X is compact ) by A14, A15, Th64, XBOOLE_0:def 4; :: thesis: verum