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