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:33;
then A1: C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:35;
A2: C is Bounded by JORDAN2C:73;
then C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is Bounded by JORDAN2C:16, XBOOLE_1:17;
hence proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed by A1, JCT_MISC:22; :: 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 bounded by A2, JCT_MISC:23, JORDAN2C:16;
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