theorem Th122: :: JGRAPH_4:122

for cn being Real
for K03 being Subset of (TOP-REAL 2) st K03 = { p where p is Point of (TOP-REAL 2) : ( p `1 >= cn * |.p.| & p `2 <= 0 ) } holds
K03 is closed