:: deftheorem defines Horizontal_Line JORDAN6:def 7 :
for s being Real holds Horizontal_Line s = { p where p is Point of (TOP-REAL 2) : p `2 = s } ;