set p1X = proj1 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A1: ( (SW-corner X) `1 = W-bound X & (NW-corner X) `1 = W-bound X ) by EUCLID:56;
(proj1 | X) .: the carrier of ((TOP-REAL 2) | X) is with_min by Def15;
then inf ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj1 | X) .: the carrier of ((TOP-REAL 2) | X) by Def4;
then consider p being set such that
A2: p in the carrier of ((TOP-REAL 2) | X) and
p in the carrier of ((TOP-REAL 2) | X) and
A3: inf ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj1 | X) . p by FUNCT_2:115;
A4: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:29;
then reconsider p = p as Point of (TOP-REAL 2) by A2;
A5: p `2 <= N-bound X by A4, A2, Lm9;
A6: ( (SW-corner X) `2 = S-bound X & (NW-corner X) `2 = N-bound X ) by EUCLID:56;
( (proj1 | X) . p = p `1 & S-bound X <= p `2 ) by A4, A2, Lm9, Th69;
then p in LSeg (SW-corner X),(NW-corner X) by A1, A6, A3, A5, GOBOARD7:8;
hence ( not W-most X is empty & W-most X is compact ) by A4, A2, Th64, XBOOLE_0:def 4; :: thesis: verum