:: deftheorem Def1 defines Sq_Circ JGRAPH_3:def 1 :
for b₁ being Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) holds
( b₁ = Sq_Circ iff for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies b₁ . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies b₁ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or b₁ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) ) );