theorem :: JGRAPH_3:27

for K0, C0 being Subset of (TOP-REAL 2) st K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & C0 = { p1 where p1 is Point of (TOP-REAL 2) : |.p1.| <= 1 } holds
Sq_Circ " C0 c= K0