let C be compact Subset of (TOP-REAL 2); :: thesis: ( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above )
set w = ((W-bound C) + (E-bound C)) / 2;
set X = C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2));
Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by JORDAN6:30;
then A1: C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8;
C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is bounded by RLTOPSP1:42, XBOOLE_1:17;
hence proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed by A1, JCT_MISC:13; :: thesis: ( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above )
C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) c= C by XBOOLE_1:17;
then proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is real-bounded by JCT_MISC:14, RLTOPSP1:42;
hence ( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above ) by XXREAL_2:def 11; :: thesis: verum