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