:: deftheorem Def13 defines west_halfline TOPREAL1:def 13 :
for p being Point of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) holds
( b₂ = west_halfline p iff for x being Point of (TOP-REAL 2) holds
( x in b₂ iff ( x `1 <= p `1 & x `2 = p `2 ) ) );