for C being compact Subset of (TOP-REAL 2) holds (north_halfline (UMP C)) \ {(UMP C)} c= UBD C