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:52;
(proj1 | X) .: the carrier of ((TOP-REAL 2) | X) is with_min
by MEASURE6:def 13;
then
lower_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
A2:
p in the carrier of ((TOP-REAL 2) | X)
and
p in the carrier of ((TOP-REAL 2) | X)
and
A3:
lower_bound ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj1 | X) . p
by FUNCT_2:64;
A4:
the carrier of ((TOP-REAL 2) | X) = X
by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A2;
A5:
p `2 <= N-bound X
by A4, A2, Lm3;
A6:
( (SW-corner X) `2 = S-bound X & (NW-corner X) `2 = N-bound X )
by EUCLID:52;
( (proj1 | X) . p = p `1 & S-bound X <= p `2 )
by A4, A2, Lm3, Th22;
then
p in LSeg ((SW-corner X),(NW-corner X))
by A1, A6, A3, A5, GOBOARD7:7;
hence
( not W-most X is empty & W-most X is compact )
by A4, A2, XBOOLE_0:def 4; verum