let C be compact Subset of (TOP-REAL 2); :: thesis: (north_halfline (UMP C)) \ {(UMP C)} misses C
set p = UMP C;
set L = north_halfline (UMP C);
set w = ((W-bound C) + (E-bound C)) / 2;
assume (north_halfline (UMP C)) \ {(UMP C)} meets C ; :: thesis: contradiction
then consider x being set such that
A1: x in (north_halfline (UMP C)) \ {(UMP C)} and
A2: x in C by XBOOLE_0:3;
A3: ( x in north_halfline (UMP C) & x <> UMP C ) by A1, ZFMISC_1:64;
reconsider x = x as Point of (TOP-REAL 2) by A1;
A4: ( x `1 = (UMP C) `1 & x `2 >= (UMP C) `2 ) by A3, TOPREAL1:def 12;
then x `2 <> (UMP C) `2 by A3, TOPREAL3:11;
then A5: x `2 > (UMP C) `2 by A4, XXREAL_0:1;
x `1 = ((W-bound C) + (E-bound C)) / 2 by A4, EUCLID:56;
then x in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN6:34;
then x in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A2, XBOOLE_0:def 4;
hence contradiction by A5, JORDAN21:41; :: thesis: verum