set p2X = proj2 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A19: ( (SW-corner X) `1 = W-bound X & (SE-corner X) `1 = E-bound X ) by EUCLID:52;
(proj2 | X) .: the carrier of ((TOP-REAL 2) | X) is left_end by MEASURE6:def 13;
then lower_bound ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj2 | X) .: the carrier of ((TOP-REAL 2) | X) by MEASURE6:def 5;
then consider p being set such that
A20: p in the carrier of ((TOP-REAL 2) | X) and
p in the carrier of ((TOP-REAL 2) | X) and
A21: lower_bound ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj2 | X) . p by FUNCT_2:64;
A22: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A20;
A23: p `1 <= E-bound X by A22, A20, Lm3;
A24: ( (SW-corner X) `2 = S-bound X & (SE-corner X) `2 = S-bound X ) by EUCLID:52;
( (proj2 | X) . p = p `2 & W-bound X <= p `1 ) by A22, A20, Lm3, Th70;
then p in LSeg ((SW-corner X),(SE-corner X)) by A19, A24, A21, A23, GOBOARD7:8;
hence ( not S-most X is empty & S-most X is compact ) by A22, A20, XBOOLE_0:def 4; :: thesis: verum