theorem Th28: :: JGRAPH_6:28

for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( not - 1 < p `1 or not p `1 < 1 or not - 1 < p `2 or not p `2 < 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| >= 1 } holds
Sq_Circ .: Kb = Cb