let C be compact Subset of (TOP-REAL 2); (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
; 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; verum