let C be compact Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st south_halfline p misses C holds
south_halfline p c= UBD C
let p be Point of (TOP-REAL 2); :: thesis: ( south_halfline p misses C implies south_halfline p c= UBD C )
set WH = south_halfline p;
assume A1: south_halfline p misses C ; :: thesis: south_halfline p c= UBD C
( not south_halfline p is bounded & not south_halfline p is empty & south_halfline p is connected ) by Th107;
hence south_halfline p c= UBD C by A1, Th109; :: thesis: verum