:: deftheorem Def10 defines north_halfline TOPREAL1:def 10 :
for p being Point of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) holds
( b₂ = north_halfline p iff for x being Point of (TOP-REAL 2) holds
( x in b₂ iff ( x `1 = p `1 & x `2 >= p `2 ) ) );