theorem Th18: :: JGRAPH_2:18

for K0a being set
for D being non empty Subset of (TOP-REAL 2) st K0a = { p where p is Point of (TOP-REAL 2) : ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) & p <> 0. (TOP-REAL 2) ) } & D ` = {(0. (TOP-REAL 2))} holds
( K0a is non empty Subset of ((TOP-REAL 2) | D) & K0a is non empty Subset of (TOP-REAL 2) )