let D be with_the_max_arc Subset of (TOP-REAL 2); :: thesis: not proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is empty
set w = ((W-bound D) + (E-bound D)) / 2;
D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2) by Def1;
then not D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2)) is empty ;
hence not proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is empty by Lm1, RELAT_1:119; :: thesis: verum