theorem Th15: :: JGRAPH_2:15

for D being Subset of (TOP-REAL 2)
for K0 being Subset of ((TOP-REAL 2) | D) st K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) ) } holds
rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)