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