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