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;
A1: ( not west_halfline p is Bounded & not west_halfline p is empty & west_halfline p is connected ) by Th128;
assume west_halfline p misses C ; :: thesis: west_halfline p c= UBD C
hence west_halfline p c= UBD C by A1, Th133; :: thesis: verum