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