:: JGRAPH_3 semantic presentation

Lemma1: for b1 being real number holds (b1 ^2 ) + 1 > 0
proof end;

Lemma2: TOP-REAL 2 = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;

Lemma3: ( dom proj1 = the carrier of (TOP-REAL 2) & dom proj2 = the carrier of (TOP-REAL 2) )
by FUNCT_2:def 1;

theorem Th1: :: JGRAPH_3:1
for b1, b2 being complex number holds
( not b1 ^2 = b2 ^2 or b1 = b2 or b1 = - b2 )
proof end;

theorem Th2: :: JGRAPH_3:2
for b1 being complex number holds
( not b1 ^2 = 1 or b1 = 1 or b1 = - 1 )
proof end;

theorem Th3: :: JGRAPH_3:3
for b1 being real number st 0 <= b1 & b1 <= 1 holds
b1 ^2 <= b1
proof end;

Lemma7: for b1, b2 being real number st b1 >= 0 & (b2 - b1) * (b2 + b1) <= 0 holds
( - b1 <= b2 & b2 <= b1 )
by XREAL_1:95;

theorem Th4: :: JGRAPH_3:4
canceled;

theorem Th5: :: JGRAPH_3:5
for b1 being real number st (b1 ^2 ) - 1 <= 0 holds
( - 1 <= b1 & b1 <= 1 )
proof end;

theorem Th6: :: JGRAPH_3:6
for b1, b2, b3 being real number holds
( ( b1 < b2 & b1 < b3 ) iff b1 < min b2,b3 )
proof end;

theorem Th7: :: JGRAPH_3:7
for b1 being real number st 0 < b1 holds
( b1 / 3 < b1 & b1 / 4 < b1 ) by XREAL_1:223, XREAL_1:225;

theorem Th8: :: JGRAPH_3:8
for b1 being real number holds
( ( b1 >= 1 implies sqrt b1 >= 1 ) & ( b1 > 1 implies sqrt b1 > 1 ) ) by SQUARE_1:83, SQUARE_1:94, SQUARE_1:95;

theorem Th9: :: JGRAPH_3:9
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
].b2,b3.[ c= ].b1,b4.[
proof end;

theorem Th10: :: JGRAPH_3:10
for b1 being Point of (TOP-REAL 2) holds
( |.b1.| = sqrt (((b1 `1 ) ^2 ) + ((b1 `2 ) ^2 )) & |.b1.| ^2 = ((b1 `1 ) ^2 ) + ((b1 `2 ) ^2 ) ) by JGRAPH_1:46, JGRAPH_1:47;

theorem Th11: :: JGRAPH_3:11
for b1 being Function
for b2, b3 being set holds (b1 | b2) .: b3 = b1 .: (b3 /\ b2)
proof end;

theorem Th12: :: JGRAPH_3:12
for b1 being TopStruct
for b2 being non empty TopStruct
for b3 being Function of b1,b2
for b4 being Subset of b1 holds b3 | b4 is Function of (b1 | b4),b2
proof end;

theorem Th13: :: JGRAPH_3:13
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being non empty Subset of b1
for b5 being non empty Subset of b2
for b6 being Function of b1,b2 st b4 ` = {b3} & b5 ` = {(b6 . b3)} & b1 is_T2 & b2 is_T2 & ( for b7 being Point of (b1 | b4) holds b6 . b7 <> b6 . b3 ) & b6 | b4 is continuous Function of (b1 | b4),(b2 | b5) & ( for b7 being Subset of b2 st b6 . b3 in b7 & b7 is open holds
ex b8 being Subset of b1 st
( b3 in b8 & b8 is open & b6 .: b8 c= b7 ) ) holds
b6 is continuous
proof end;

definition
func Sq_Circ -> Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) means :Def1: :: JGRAPH_3:def 1
for b1 being Point of (TOP-REAL 2) holds
( ( b1 = 0.REAL 2 implies a1 . b1 = b1 ) & ( ( ( b1 `2 <= b1 `1 & - (b1 `1 ) <= b1 `2 ) or ( b1 `2 >= b1 `1 & b1 `2 <= - (b1 `1 ) ) ) & b1 <> 0.REAL 2 implies a1 . b1 = |[((b1 `1 ) / (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 )))),((b1 `2 ) / (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 ))))]| ) & ( ( b1 `2 <= b1 `1 & - (b1 `1 ) <= b1 `2 ) or ( b1 `2 >= b1 `1 & b1 `2 <= - (b1 `1 ) ) or not b1 <> 0.REAL 2 or a1 . b1 = |[((b1 `1 ) / (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 )))),((b1 `2 ) / (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 ))))]| ) );
existence
ex b1 being Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) st
for b2 being Point of (TOP-REAL 2) holds
( ( b2 = 0.REAL 2 implies b1 . b2 = b2 ) & ( ( ( b2 `2 <= b2 `1 & - (b2 `1 ) <= b2 `2 ) or ( b2 `2 >= b2 `1 & b2 `2 <= - (b2 `1 ) ) ) & b2 <> 0.REAL 2 implies b1 . b2 = |[((b2 `1 ) / (sqrt (1 + (((b2 `2 ) / (b2 `1 )) ^2 )))),((b2 `2 ) / (sqrt (1 + (((b2 `2 ) / (b2 `1 )) ^2 ))))]| ) & ( ( b2 `2 <= b2 `1 & - (b2 `1 ) <= b2 `2 ) or ( b2 `2 >= b2 `1 & b2 `2 <= - (b2 `1 ) ) or not b2 <> 0.REAL 2 or b1 . b2 = |[((b2 `1 ) / (sqrt (1 + (((b2 `1 ) / (b2 `2 )) ^2 )))),((b2 `2 ) / (sqrt (1 + (((b2 `1 ) / (b2 `2 )) ^2 ))))]| ) )
proof end;
uniqueness
for b1, b2 being Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) st ( for b3 being Point of (TOP-REAL 2) holds
( ( b3 = 0.REAL 2 implies b1 . b3 = b3 ) & ( ( ( b3 `2 <= b3 `1 & - (b3 `1 ) <= b3 `2 ) or ( b3 `2 >= b3 `1 & b3 `2 <= - (b3 `1 ) ) ) & b3 <> 0.REAL 2 implies b1 . b3 = |[((b3 `1 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 )))),((b3 `2 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 ))))]| ) & ( ( b3 `2 <= b3 `1 & - (b3 `1 ) <= b3 `2 ) or ( b3 `2 >= b3 `1 & b3 `2 <= - (b3 `1 ) ) or not b3 <> 0.REAL 2 or b1 . b3 = |[((b3 `1 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 )))),((b3 `2 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 ))))]| ) ) ) & ( for b3 being Point of (TOP-REAL 2) holds
( ( b3 = 0.REAL 2 implies b2 . b3 = b3 ) & ( ( ( b3 `2 <= b3 `1 & - (b3 `1 ) <= b3 `2 ) or ( b3 `2 >= b3 `1 & b3 `2 <= - (b3 `1 ) ) ) & b3 <> 0.REAL 2 implies b2 . b3 = |[((b3 `1 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 )))),((b3 `2 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 ))))]| ) & ( ( b3 `2 <= b3 `1 & - (b3 `1 ) <= b3 `2 ) or ( b3 `2 >= b3 `1 & b3 `2 <= - (b3 `1 ) ) or not b3 <> 0.REAL 2 or b2 . b3 = |[((b3 `1 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 )))),((b3 `2 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 ))))]| ) ) ) holds
b1 = b2
proof end;
end;

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

theorem Th14: :: JGRAPH_3:14
for b1 being Point of (TOP-REAL 2) st b1 <> 0.REAL 2 holds
( ( ( ( b1 `1 <= b1 `2 & - (b1 `2 ) <= b1 `1 ) or ( b1 `1 >= b1 `2 & b1 `1 <= - (b1 `2 ) ) ) implies Sq_Circ . b1 = |[((b1 `1 ) / (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 )))),((b1 `2 ) / (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 ))))]| ) & ( ( b1 `1 <= b1 `2 & - (b1 `2 ) <= b1 `1 ) or ( b1 `1 >= b1 `2 & b1 `1 <= - (b1 `2 ) ) or Sq_Circ . b1 = |[((b1 `1 ) / (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 )))),((b1 `2 ) / (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 ))))]| ) )
proof end;

theorem Th15: :: JGRAPH_3:15
for b1 being non empty TopSpace
for b2 being Function of b1,R^1 st b2 is continuous & ( for b3 being Point of b1 ex b4 being real number st
( b2 . b3 = b4 & b4 >= 0 ) ) holds
ex b3 being Function of b1,R^1 st
( ( for b4 being Point of b1
for b5 being real number st b2 . b4 = b5 holds
b3 . b4 = sqrt b5 ) & b3 is continuous )
proof end;

theorem Th16: :: JGRAPH_3:16
for b1 being non empty TopSpace
for b2, b3 being Function of b1,R^1 st b2 is continuous & b3 is continuous & ( for b4 being Point of b1 holds b3 . b4 <> 0 ) holds
ex b4 being Function of b1,R^1 st
( ( for b5 being Point of b1
for b6, b7 being real number st b2 . b5 = b6 & b3 . b5 = b7 holds
b4 . b5 = (b6 / b7) ^2 ) & b4 is continuous )
proof end;

theorem Th17: :: JGRAPH_3:17
for b1 being non empty TopSpace
for b2, b3 being Function of b1,R^1 st b2 is continuous & b3 is continuous & ( for b4 being Point of b1 holds b3 . b4 <> 0 ) holds
ex b4 being Function of b1,R^1 st
( ( for b5 being Point of b1
for b6, b7 being real number st b2 . b5 = b6 & b3 . b5 = b7 holds
b4 . b5 = 1 + ((b6 / b7) ^2 ) ) & b4 is continuous )
proof end;

theorem Th18: :: JGRAPH_3:18
for b1 being non empty TopSpace
for b2, b3 being Function of b1,R^1 st b2 is continuous & b3 is continuous & ( for b4 being Point of b1 holds b3 . b4 <> 0 ) holds
ex b4 being Function of b1,R^1 st
( ( for b5 being Point of b1
for b6, b7 being real number st b2 . b5 = b6 & b3 . b5 = b7 holds
b4 . b5 = sqrt (1 + ((b6 / b7) ^2 )) ) & b4 is continuous )
proof end;

theorem Th19: :: JGRAPH_3:19
for b1 being non empty TopSpace
for b2, b3 being Function of b1,R^1 st b2 is continuous & b3 is continuous & ( for b4 being Point of b1 holds b3 . b4 <> 0 ) holds
ex b4 being Function of b1,R^1 st
( ( for b5 being Point of b1
for b6, b7 being real number st b2 . b5 = b6 & b3 . b5 = b7 holds
b4 . b5 = b6 / (sqrt (1 + ((b6 / b7) ^2 ))) ) & b4 is continuous )
proof end;

theorem Th20: :: JGRAPH_3:20
for b1 being non empty TopSpace
for b2, b3 being Function of b1,R^1 st b2 is continuous & b3 is continuous & ( for b4 being Point of b1 holds b3 . b4 <> 0 ) holds
ex b4 being Function of b1,R^1 st
( ( for b5 being Point of b1
for b6, b7 being real number st b2 . b5 = b6 & b3 . b5 = b7 holds
b4 . b5 = b7 / (sqrt (1 + ((b6 / b7) ^2 ))) ) & b4 is continuous )
proof end;

Lemma23: for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Point of ((TOP-REAL 2) | b1) holds (proj2 | b1) . b2 = proj2 . b2
proof end;

Lemma24: for b1 being non empty Subset of (TOP-REAL 2) holds proj2 | b1 is continuous Function of ((TOP-REAL 2) | b1),R^1
proof end;

Lemma25: for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Point of ((TOP-REAL 2) | b1) holds (proj1 | b1) . b2 = proj1 . b2
proof end;

Lemma26: for b1 being non empty Subset of (TOP-REAL 2) holds proj1 | b1 is continuous Function of ((TOP-REAL 2) | b1),R^1
proof end;

theorem Th21: :: JGRAPH_3:21
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Function of ((TOP-REAL 2) | b1),R^1 st ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b2 . b3 = (b3 `1 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 ))) ) & ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b3 `1 <> 0 ) holds
b2 is continuous
proof end;

theorem Th22: :: JGRAPH_3:22
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Function of ((TOP-REAL 2) | b1),R^1 st ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b2 . b3 = (b3 `2 ) / (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 ))) ) & ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b3 `1 <> 0 ) holds
b2 is continuous
proof end;

theorem Th23: :: JGRAPH_3:23
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Function of ((TOP-REAL 2) | b1),R^1 st ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b2 . b3 = (b3 `2 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 ))) ) & ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b3 `2 <> 0 ) holds
b2 is continuous
proof end;

theorem Th24: :: JGRAPH_3:24
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Function of ((TOP-REAL 2) | b1),R^1 st ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b2 . b3 = (b3 `1 ) / (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 ))) ) & ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b3 `2 <> 0 ) holds
b2 is continuous
proof end;

Lemma31: ( ( ( (1.REAL 2) `2 <= (1.REAL 2) `1 & - ((1.REAL 2) `1 ) <= (1.REAL 2) `2 ) or ( (1.REAL 2) `2 >= (1.REAL 2) `1 & (1.REAL 2) `2 <= - ((1.REAL 2) `1 ) ) ) & 1.REAL 2 <> 0.REAL 2 )
by JGRAPH_2:13, REVROT_1:19;

Lemma32: for b1 being non empty Subset of (TOP-REAL 2) holds dom (proj2 * (Sq_Circ | b1)) = the carrier of ((TOP-REAL 2) | b1)
proof end;

Lemma33: for b1 being non empty Subset of (TOP-REAL 2) holds dom (proj1 * (Sq_Circ | b1)) = the carrier of ((TOP-REAL 2) | b1)
proof end;

Lemma34: the carrier of (TOP-REAL 2) \ {(0.REAL 2)} <> {}
by JGRAPH_2:19;

theorem Th25: :: JGRAPH_3:25
for b1, b2 being Subset of (TOP-REAL 2)
for b3 being Function of ((TOP-REAL 2) | b1),((TOP-REAL 2) | b2) st b3 = Sq_Circ | b1 & b2 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b1 = { b4 where B is Point of (TOP-REAL 2) : ( ( ( b4 `2 <= b4 `1 & - (b4 `1 ) <= b4 `2 ) or ( b4 `2 >= b4 `1 & b4 `2 <= - (b4 `1 ) ) ) & b4 <> 0.REAL 2 ) } holds
b3 is continuous
proof end;

Lemma36: ( ( ( (1.REAL 2) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2 ) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2 ) ) ) & 1.REAL 2 <> 0.REAL 2 )
by JGRAPH_2:13, REVROT_1:19;

theorem Th26: :: JGRAPH_3:26
for b1, b2 being Subset of (TOP-REAL 2)
for b3 being Function of ((TOP-REAL 2) | b1),((TOP-REAL 2) | b2) st b3 = Sq_Circ | b1 & b2 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b1 = { b4 where B is Point of (TOP-REAL 2) : ( ( ( b4 `1 <= b4 `2 & - (b4 `2 ) <= b4 `1 ) or ( b4 `1 >= b4 `2 & b4 `1 <= - (b4 `2 ) ) ) & b4 <> 0.REAL 2 ) } holds
b3 is continuous
proof end;

scheme :: JGRAPH_3:sch 1
s1{ P1[ set ] } :
{ b1 where B is Point of (TOP-REAL 2) : ( P1[b1] & b1 <> 0.REAL 2 ) } c= the carrier of (TOP-REAL 2) \ {(0.REAL 2)}
proof end;

scheme :: JGRAPH_3:sch 2
s2{ P1[ set ] } :
{ b1 where B is Point of (TOP-REAL 2) : ( P1[b1] & b1 <> 0.REAL 2 ) } = { b1 where B is Point of (TOP-REAL 2) : P1[b1] } /\ (the carrier of (TOP-REAL 2) \ {(0.REAL 2)})
proof end;

theorem Th27: :: JGRAPH_3:27
for b1 being Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3 being Function of (((TOP-REAL 2) | b1) | b2),((TOP-REAL 2) | b1) st b3 = Sq_Circ | b2 & b1 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b2 = { b4 where B is Point of (TOP-REAL 2) : ( ( ( b4 `2 <= b4 `1 & - (b4 `1 ) <= b4 `2 ) or ( b4 `2 >= b4 `1 & b4 `2 <= - (b4 `1 ) ) ) & b4 <> 0.REAL 2 ) } holds
( b3 is continuous & b2 is closed )
proof end;

theorem Th28: :: JGRAPH_3:28
for b1 being Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3 being Function of (((TOP-REAL 2) | b1) | b2),((TOP-REAL 2) | b1) st b3 = Sq_Circ | b2 & b1 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b2 = { b4 where B is Point of (TOP-REAL 2) : ( ( ( b4 `1 <= b4 `2 & - (b4 `2 ) <= b4 `1 ) or ( b4 `1 >= b4 `2 & b4 `1 <= - (b4 `2 ) ) ) & b4 <> 0.REAL 2 ) } holds
( b3 is continuous & b2 is closed )
proof end;

theorem Th29: :: JGRAPH_3:29
for b1 being non empty Subset of (TOP-REAL 2) st b1 ` = {(0.REAL 2)} holds
ex b2 being Function of ((TOP-REAL 2) | b1),((TOP-REAL 2) | b1) st
( b2 = Sq_Circ | b1 & b2 is continuous )
proof end;

theorem Th30: :: JGRAPH_3:30
for b1 being non empty Subset of (TOP-REAL 2) st b1 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} holds
b1 ` = {(0.REAL 2)}
proof end;

theorem Th31: :: JGRAPH_3:31
ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b1 = Sq_Circ & b1 is continuous )
proof end;

theorem Th32: :: JGRAPH_3:32
Sq_Circ is one-to-one
proof end;

registration
cluster Sq_Circ -> one-to-one ;
coherence
Sq_Circ is one-to-one
by Th32;
end;

theorem Th33: :: JGRAPH_3:33
for b1, b2 being Subset of (TOP-REAL 2) st b1 = { b3 where B is Point of (TOP-REAL 2) : ( ( - 1 = b3 `1 & - 1 <= b3 `2 & b3 `2 <= 1 ) or ( b3 `1 = 1 & - 1 <= b3 `2 & b3 `2 <= 1 ) or ( - 1 = b3 `2 & - 1 <= b3 `1 & b3 `1 <= 1 ) or ( 1 = b3 `2 & - 1 <= b3 `1 & b3 `1 <= 1 ) ) } & b2 = { b3 where B is Point of (TOP-REAL 2) : |.b3.| = 1 } holds
Sq_Circ .: b1 = b2
proof end;

theorem Th34: :: JGRAPH_3:34
for b1, b2 being Subset of (TOP-REAL 2)
for b3 being Function of ((TOP-REAL 2) | b2),((TOP-REAL 2) | b1) st b2 = { b4 where B is Point of (TOP-REAL 2) : ( ( - 1 = b4 `1 & - 1 <= b4 `2 & b4 `2 <= 1 ) or ( b4 `1 = 1 & - 1 <= b4 `2 & b4 `2 <= 1 ) or ( - 1 = b4 `2 & - 1 <= b4 `1 & b4 `1 <= 1 ) or ( 1 = b4 `2 & - 1 <= b4 `1 & b4 `1 <= 1 ) ) } & b3 is_homeomorphism holds
b1 is_simple_closed_curve
proof end;

theorem Th35: :: JGRAPH_3:35
for b1 being Subset of (TOP-REAL 2) st b1 = { b2 where B is Point of (TOP-REAL 2) : ( ( - 1 = b2 `1 & - 1 <= b2 `2 & b2 `2 <= 1 ) or ( b2 `1 = 1 & - 1 <= b2 `2 & b2 `2 <= 1 ) or ( - 1 = b2 `2 & - 1 <= b2 `1 & b2 `1 <= 1 ) or ( 1 = b2 `2 & - 1 <= b2 `1 & b2 `1 <= 1 ) ) } holds
( b1 is_simple_closed_curve & b1 is compact )
proof end;

theorem Th36: :: JGRAPH_3:36
for b1 being Subset of (TOP-REAL 2) st b1 = { b2 where B is Point of (TOP-REAL 2) : |.b2.| = 1 } holds
b1 is_simple_closed_curve
proof end;

theorem Th37: :: JGRAPH_3:37
for b1, b2 being Subset of (TOP-REAL 2) st b1 = { b3 where B is Point of (TOP-REAL 2) : ( - 1 <= b3 `1 & b3 `1 <= 1 & - 1 <= b3 `2 & b3 `2 <= 1 ) } & b2 = { b3 where B is Point of (TOP-REAL 2) : |.b3.| <= 1 } holds
Sq_Circ " b2 c= b1
proof end;

theorem Th38: :: JGRAPH_3:38
for b1 being Point of (TOP-REAL 2) holds
( ( b1 = 0.REAL 2 implies (Sq_Circ " ) . b1 = 0.REAL 2 ) & ( ( ( b1 `2 <= b1 `1 & - (b1 `1 ) <= b1 `2 ) or ( b1 `2 >= b1 `1 & b1 `2 <= - (b1 `1 ) ) ) & b1 <> 0.REAL 2 implies (Sq_Circ " ) . b1 = |[((b1 `1 ) * (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 )))),((b1 `2 ) * (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 ))))]| ) & ( ( b1 `2 <= b1 `1 & - (b1 `1 ) <= b1 `2 ) or ( b1 `2 >= b1 `1 & b1 `2 <= - (b1 `1 ) ) or not b1 <> 0.REAL 2 or (Sq_Circ " ) . b1 = |[((b1 `1 ) * (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 )))),((b1 `2 ) * (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 ))))]| ) )
proof end;

theorem Th39: :: JGRAPH_3:39
Sq_Circ " is Function of (TOP-REAL 2),(TOP-REAL 2)
proof end;

theorem Th40: :: JGRAPH_3:40
for b1 being Point of (TOP-REAL 2) st b1 <> 0.REAL 2 holds
( ( ( ( b1 `1 <= b1 `2 & - (b1 `2 ) <= b1 `1 ) or ( b1 `1 >= b1 `2 & b1 `1 <= - (b1 `2 ) ) ) implies (Sq_Circ " ) . b1 = |[((b1 `1 ) * (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 )))),((b1 `2 ) * (sqrt (1 + (((b1 `1 ) / (b1 `2 )) ^2 ))))]| ) & ( ( b1 `1 <= b1 `2 & - (b1 `2 ) <= b1 `1 ) or ( b1 `1 >= b1 `2 & b1 `1 <= - (b1 `2 ) ) or (Sq_Circ " ) . b1 = |[((b1 `1 ) * (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 )))),((b1 `2 ) * (sqrt (1 + (((b1 `2 ) / (b1 `1 )) ^2 ))))]| ) )
proof end;

theorem Th41: :: JGRAPH_3:41
for b1 being non empty TopSpace
for b2, b3 being Function of b1,R^1 st b2 is continuous & b3 is continuous & ( for b4 being Point of b1 holds b3 . b4 <> 0 ) holds
ex b4 being Function of b1,R^1 st
( ( for b5 being Point of b1
for b6, b7 being real number st b2 . b5 = b6 & b3 . b5 = b7 holds
b4 . b5 = b6 * (sqrt (1 + ((b6 / b7) ^2 ))) ) & b4 is continuous )
proof end;

theorem Th42: :: JGRAPH_3:42
for b1 being non empty TopSpace
for b2, b3 being Function of b1,R^1 st b2 is continuous & b3 is continuous & ( for b4 being Point of b1 holds b3 . b4 <> 0 ) holds
ex b4 being Function of b1,R^1 st
( ( for b5 being Point of b1
for b6, b7 being real number st b2 . b5 = b6 & b3 . b5 = b7 holds
b4 . b5 = b7 * (sqrt (1 + ((b6 / b7) ^2 ))) ) & b4 is continuous )
proof end;

theorem Th43: :: JGRAPH_3:43
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Function of ((TOP-REAL 2) | b1),R^1 st ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b2 . b3 = (b3 `1 ) * (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 ))) ) & ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b3 `1 <> 0 ) holds
b2 is continuous
proof end;

theorem Th44: :: JGRAPH_3:44
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Function of ((TOP-REAL 2) | b1),R^1 st ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b2 . b3 = (b3 `2 ) * (sqrt (1 + (((b3 `2 ) / (b3 `1 )) ^2 ))) ) & ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b3 `1 <> 0 ) holds
b2 is continuous
proof end;

theorem Th45: :: JGRAPH_3:45
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Function of ((TOP-REAL 2) | b1),R^1 st ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b2 . b3 = (b3 `2 ) * (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 ))) ) & ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b3 `2 <> 0 ) holds
b2 is continuous
proof end;

theorem Th46: :: JGRAPH_3:46
for b1 being non empty Subset of (TOP-REAL 2)
for b2 being Function of ((TOP-REAL 2) | b1),R^1 st ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b2 . b3 = (b3 `1 ) * (sqrt (1 + (((b3 `1 ) / (b3 `2 )) ^2 ))) ) & ( for b3 being Point of (TOP-REAL 2) st b3 in the carrier of ((TOP-REAL 2) | b1) holds
b3 `2 <> 0 ) holds
b2 is continuous
proof end;

Lemma56: for b1 being non empty Subset of (TOP-REAL 2) holds proj2 * ((Sq_Circ " ) | b1) is Function of ((TOP-REAL 2) | b1),R^1
proof end;

Lemma57: for b1 being non empty Subset of (TOP-REAL 2) holds proj1 * ((Sq_Circ " ) | b1) is Function of ((TOP-REAL 2) | b1),R^1
proof end;

theorem Th47: :: JGRAPH_3:47
for b1, b2 being Subset of (TOP-REAL 2)
for b3 being Function of ((TOP-REAL 2) | b1),((TOP-REAL 2) | b2) st b3 = (Sq_Circ " ) | b1 & b2 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b1 = { b4 where B is Point of (TOP-REAL 2) : ( ( ( b4 `2 <= b4 `1 & - (b4 `1 ) <= b4 `2 ) or ( b4 `2 >= b4 `1 & b4 `2 <= - (b4 `1 ) ) ) & b4 <> 0.REAL 2 ) } holds
b3 is continuous
proof end;

theorem Th48: :: JGRAPH_3:48
for b1, b2 being Subset of (TOP-REAL 2)
for b3 being Function of ((TOP-REAL 2) | b1),((TOP-REAL 2) | b2) st b3 = (Sq_Circ " ) | b1 & b2 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b1 = { b4 where B is Point of (TOP-REAL 2) : ( ( ( b4 `1 <= b4 `2 & - (b4 `2 ) <= b4 `1 ) or ( b4 `1 >= b4 `2 & b4 `1 <= - (b4 `2 ) ) ) & b4 <> 0.REAL 2 ) } holds
b3 is continuous
proof end;

theorem Th49: :: JGRAPH_3:49
for b1 being Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3 being Function of (((TOP-REAL 2) | b1) | b2),((TOP-REAL 2) | b1) st b3 = (Sq_Circ " ) | b2 & b1 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b2 = { b4 where B is Point of (TOP-REAL 2) : ( ( ( b4 `2 <= b4 `1 & - (b4 `1 ) <= b4 `2 ) or ( b4 `2 >= b4 `1 & b4 `2 <= - (b4 `1 ) ) ) & b4 <> 0.REAL 2 ) } holds
( b3 is continuous & b2 is closed )
proof end;

theorem Th50: :: JGRAPH_3:50
for b1 being Subset of (TOP-REAL 2)
for b2 being Subset of ((TOP-REAL 2) | b1)
for b3 being Function of (((TOP-REAL 2) | b1) | b2),((TOP-REAL 2) | b1) st b3 = (Sq_Circ " ) | b2 & b1 = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} & b2 = { b4 where B is Point of (TOP-REAL 2) : ( ( ( b4 `1 <= b4 `2 & - (b4 `2 ) <= b4 `1 ) or ( b4 `1 >= b4 `2 & b4 `1 <= - (b4 `2 ) ) ) & b4 <> 0.REAL 2 ) } holds
( b3 is continuous & b2 is closed )
proof end;

theorem Th51: :: JGRAPH_3:51
for b1 being non empty Subset of (TOP-REAL 2) st b1 ` = {(0.REAL 2)} holds
ex b2 being Function of ((TOP-REAL 2) | b1),((TOP-REAL 2) | b1) st
( b2 = (Sq_Circ " ) | b1 & b2 is continuous )
proof end;

theorem Th52: :: JGRAPH_3:52
ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b1 = Sq_Circ " & b1 is continuous )
proof end;

Lemma64: Sq_Circ " is one-to-one
by FUNCT_1:62;

theorem Th53: :: JGRAPH_3:53
canceled;

theorem Th54: :: JGRAPH_3:54
( Sq_Circ is Function of (TOP-REAL 2),(TOP-REAL 2) & rng Sq_Circ = the carrier of (TOP-REAL 2) & ( for b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st b1 = Sq_Circ holds
b1 is_homeomorphism ) )
proof end;

E66: now
let c1, c2 be real number ;
assume (((c1 ^2 ) + (c2 ^2 )) - 1) * (c1 ^2 ) <= c2 ^2 ;
then (((c1 ^2 ) * (c1 ^2 )) + ((c1 ^2 ) * ((c2 ^2 ) - 1))) - (c2 ^2 ) <= (c2 ^2 ) - (c2 ^2 ) by XREAL_1:11;
hence ((c1 ^2 ) - 1) * ((c1 ^2 ) + (c2 ^2 )) <= 0 ;
end;

E67: now
let c1 be real number ;
assume (c1 ^2 ) - 1 = 0 ;
then (c1 - 1) * (c1 + 1) = 0 ;
then ( c1 - 1 = 0 or c1 + 1 = 0 ) by XCMPLX_1:6;
then ( c1 = 0 + 1 or c1 + 1 = 0 ) ;
then ( c1 = 1 or c1 = 0 - 1 ) ;
hence ( c1 = 1 or c1 = - 1 ) ;
end;

theorem Th55: :: JGRAPH_3:55
for b1, b2 being Function of I[01] ,(TOP-REAL 2)
for b3, b4, b5, b6, b7 being Subset of (TOP-REAL 2)
for b8, b9 being Point of I[01] st b8 = 0 & b9 = 1 & b1 is continuous & b1 is one-to-one & b2 is continuous & b2 is one-to-one & b3 = { b10 where B is Point of (TOP-REAL 2) : |.b10.| <= 1 } & b4 = { b10 where B is Point of (TOP-REAL 2) : ( |.b10.| = 1 & b10 `2 <= b10 `1 & b10 `2 >= - (b10 `1 ) ) } & b5 = { b10 where B is Point of (TOP-REAL 2) : ( |.b10.| = 1 & b10 `2 >= b10 `1 & b10 `2 <= - (b10 `1 ) ) } & b6 = { b10 where B is Point of (TOP-REAL 2) : ( |.b10.| = 1 & b10 `2 >= b10 `1 & b10 `2 >= - (b10 `1 ) ) } & b7 = { b10 where B is Point of (TOP-REAL 2) : ( |.b10.| = 1 & b10 `2 <= b10 `1 & b10 `2 <= - (b10 `1 ) ) } & b1 . b8 in b5 & b1 . b9 in b4 & b2 . b8 in b7 & b2 . b9 in b6 & rng b1 c= b3 & rng b2 c= b3 holds
rng b1 meets rng b2
proof end;