let C be compact Subset of (TOP-REAL 2); :: thesis: (south_halfline (LMP C)) \ {(LMP C)} misses C
set p = LMP C;
set L = south_halfline (LMP C);
set w = ((W-bound C) + (E-bound C)) / 2;
assume (south_halfline (LMP C)) \ {(LMP C)} meets C ; :: thesis: contradiction
then consider x being object such that
A1: x in (south_halfline (LMP C)) \ {(LMP C)} and
A2: x in C by XBOOLE_0:3;
A3: x in south_halfline (LMP C) by A1, ZFMISC_1:56;
A4: x <> LMP C by A1, ZFMISC_1:56;
reconsider x = x as Point of (TOP-REAL 2) by A1;
A5: x `1 = (LMP C) `1 by A3, TOPREAL1:def 12;
A6: x `2 <= (LMP C) `2 by A3, TOPREAL1:def 12;
x `2 <> (LMP C) `2 by A4, A5, TOPREAL3:6;
then A7: x `2 < (LMP 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:29; :: thesis: verum