theorem Th123: :: JGRAPH_4:123

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