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 object 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) by A1, ZFMISC_1:56;
A4: x <> UMP C by A1, ZFMISC_1:56;
reconsider x = x as Point of (TOP-REAL 2) by A1;
A5: x `1 = (UMP C) `1 by A3, TOPREAL1:def 10;
A6: x `2 >= (UMP C) `2 by A3, TOPREAL1:def 10;
x `2 <> (UMP C) `2 by A4, A5, TOPREAL3:6;
then A7: x `2 > (UMP C) `2 by A6, XXREAL_0:1;
x `1 = ((W-bound C) + (E-bound C)) / 2 by A5, EUCLID:52;
then x in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by JORDAN6:31;
then x in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A2, XBOOLE_0:def 4;
hence contradiction by A7, JORDAN21:28; :: thesis: verum