theorem Th23: :: JGRAPH_3:23

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