theorem :: JORDAN6:32

for r being Real
for p being Point of (TOP-REAL 2) holds
( p in Horizontal_Line r iff p `2 = r )