:: On the Simple Closed Curve Property of the Circle and the Fashoda Meet Theorem for It
:: by Yatsuka Nakamura
::
:: Copyright (c) 2001-2021 Association of Mizar Users

Lm1: for x being Real holds (x ^2) + 1 > 0
proof end;

Lm2: dom proj1 = the carrier of ()
by FUNCT_2:def 1;

Lm3: dom proj2 = the carrier of ()
by FUNCT_2:def 1;

theorem :: JGRAPH_3:1
for p being Point of () holds
( |.p.| = sqrt (((p 1) ^2) + ((p 2) ^2)) & |.p.| ^2 = ((p 1) ^2) + ((p 2) ^2) ) by ;

theorem :: JGRAPH_3:2
for f being Function
for B, C being set holds (f | B) .: C = f .: (C /\ B)
proof end;

theorem Th3: :: JGRAPH_3:3
for X, Y being non empty TopSpace
for p0 being Point of X
for D being non empty Subset of X
for E being non empty Subset of Y
for f being Function of X,Y st D  = {p0} & E  = {(f . p0)} & X is T_2 & Y is T_2 & ( for p being Point of (X | D) holds f . p <> f . p0 ) & f | D is continuous Function of (X | D),(Y | E) & ( for V being Subset of Y st f . p0 in V & V is open holds
ex W being Subset of X st
( p0 in W & W is open & f .: W c= V ) ) holds
f is continuous
proof end;

definition
func Sq_Circ -> Function of the carrier of (), the carrier of () means :Def1: :: JGRAPH_3:def 1
for p being Point of () holds
( ( p = 0. () implies it . p = p ) & ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () implies it . 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. () or it . p = |[((p 1) / (sqrt (1 + (((p 1) / (p 2)) ^2)))),((p 2) / (sqrt (1 + (((p 1) / (p 2)) ^2))))]| ) );
existence
ex b1 being Function of the carrier of (), the carrier of () st
for p being Point of () holds
( ( p = 0. () implies b1 . p = p ) & ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () implies b1 . 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. () or b1 . p = |[((p 1) / (sqrt (1 + (((p 1) / (p 2)) ^2)))),((p 2) / (sqrt (1 + (((p 1) / (p 2)) ^2))))]| ) )
proof end;
uniqueness
for b1, b2 being Function of the carrier of (), the carrier of () st ( for p being Point of () holds
( ( p = 0. () implies b1 . p = p ) & ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () implies b1 . 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. () or b1 . p = |[((p 1) / (sqrt (1 + (((p 1) / (p 2)) ^2)))),((p 2) / (sqrt (1 + (((p 1) / (p 2)) ^2))))]| ) ) ) & ( for p being Point of () holds
( ( p = 0. () implies b2 . p = p ) & ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () implies b2 . 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. () or b2 . p = |[((p 1) / (sqrt (1 + (((p 1) / (p 2)) ^2)))),((p 2) / (sqrt (1 + (((p 1) / (p 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 (), the carrier of () holds
( b1 = Sq_Circ iff for p being Point of () holds
( ( p = 0. () implies b1 . p = p ) & ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () implies b1 . 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. () or b1 . p = |[((p 1) / (sqrt (1 + (((p 1) / (p 2)) ^2)))),((p 2) / (sqrt (1 + (((p 1) / (p 2)) ^2))))]| ) ) );

theorem Th4: :: JGRAPH_3:4
for p being Point of () st p <> 0. () holds
( ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) implies Sq_Circ . p = |[((p 1) / (sqrt (1 + (((p 1) / (p 2)) ^2)))),((p 2) / (sqrt (1 + (((p 1) / (p 2)) ^2))))]| ) & ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) or Sq_Circ . p = |[((p 1) / (sqrt (1 + (((p 2) / (p 1)) ^2)))),((p 2) / (sqrt (1 + (((p 2) / (p 1)) ^2))))]| ) )
proof end;

theorem Th5: :: JGRAPH_3:5
for X being non empty TopSpace
for f1 being Function of X,R^1 st f1 is continuous & ( for q being Point of X ex r being Real st
( f1 . q = r & r >= 0 ) ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = sqrt r1 ) & g is continuous )
proof end;

theorem Th6: :: JGRAPH_3:6
for X being non empty TopSpace
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = (r1 / r2) ^2 ) & g is continuous )
proof end;

theorem Th7: :: JGRAPH_3:7
for X being non empty TopSpace
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = 1 + ((r1 / r2) ^2) ) & g is continuous )
proof end;

theorem Th8: :: JGRAPH_3:8
for X being non empty TopSpace
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = sqrt (1 + ((r1 / r2) ^2)) ) & g is continuous )
proof end;

theorem Th9: :: JGRAPH_3:9
for X being non empty TopSpace
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )
proof end;

theorem Th10: :: JGRAPH_3:10
for X being non empty TopSpace
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r2 / (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )
proof end;

Lm4: for K1 being non empty Subset of ()
for q being Point of (() | K1) holds (proj2 | K1) . q = proj2 . q

proof end;

Lm5: for K1 being non empty Subset of () holds proj2 | K1 is continuous Function of (() | K1),R^1
proof end;

Lm6: for K1 being non empty Subset of ()
for q being Point of (() | K1) holds (proj1 | K1) . q = proj1 . q

proof end;

Lm7: for K1 being non empty Subset of () holds proj1 | K1 is continuous Function of (() | K1),R^1
proof end;

theorem Th11: :: JGRAPH_3:11
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = (p 1) / (sqrt (1 + (((p 2) / (p 1)) ^2))) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 1 <> 0 ) holds
f is continuous
proof end;

theorem Th12: :: JGRAPH_3:12
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = (p 2) / (sqrt (1 + (((p 2) / (p 1)) ^2))) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 1 <> 0 ) holds
f is continuous
proof end;

theorem Th13: :: JGRAPH_3:13
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = (p 2) / (sqrt (1 + (((p 1) / (p 2)) ^2))) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 2 <> 0 ) holds
f is continuous
proof end;

theorem Th14: :: JGRAPH_3:14
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = (p 1) / (sqrt (1 + (((p 1) / (p 2)) ^2))) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 2 <> 0 ) holds
f is continuous
proof end;

Lm8: 0.REAL 2 = 0. ()
by EUCLID:66;

Lm9: ( ( () 2 <= () 1 & - (() 1) <= () 2 ) or ( () 2 >= () 1 & () 2 <= - (() 1) ) )
by JGRAPH_2:5;

Lm10: 1.REAL 2 <> 0. ()
by ;

Lm11: for K1 being non empty Subset of () holds dom (proj2 * (Sq_Circ | K1)) = the carrier of (() | K1)
proof end;

Lm12: for K1 being non empty Subset of () holds dom (proj1 * (Sq_Circ | K1)) = the carrier of (() | K1)
proof end;

Lm13:
by JGRAPH_2:9;

theorem Th15: :: JGRAPH_3:15
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () ) } holds
f is continuous
proof end;

Lm14: ( ( () 1 <= () 2 & - (() 2) <= () 1 ) or ( () 1 >= () 2 & () 1 <= - (() 2) ) )
by JGRAPH_2:5;

Lm15: 1.REAL 2 <> 0. ()
by ;

theorem Th16: :: JGRAPH_3:16
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) & p <> 0. () ) } holds
f is continuous
proof end;

scheme :: JGRAPH_3:sch 1
TopIncl{ P1[ set ] } :
{ p where p is Point of () : ( P1[p] & p <> 0. () ) } c= NonZero ()
proof end;

scheme :: JGRAPH_3:sch 2
TopInter{ P1[ set ] } :
{ p where p is Point of () : ( P1[p] & p <> 0. () ) } = { p7 where p7 is Point of () : P1[p7] } /\ (NonZero ())
proof end;

theorem Th17: :: JGRAPH_3:17
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () ) } holds
( f is continuous & K0 is closed )
proof end;

theorem Th18: :: JGRAPH_3:18
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) & p <> 0. () ) } holds
( f is continuous & K0 is closed )
proof end;

theorem Th19: :: JGRAPH_3:19
for D being non empty Subset of () st D  = {(0. ())} holds
ex h being Function of (() | D),(() | D) st
( h = Sq_Circ | D & h is continuous )
proof end;

theorem Th20: :: JGRAPH_3:20
for D being non empty Subset of () st D = NonZero () holds
D  = {(0. ())}
proof end;

Lm16: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr ()
by EUCLID:def 8;

theorem Th21: :: JGRAPH_3:21
ex h being Function of (),() st
( h = Sq_Circ & h is continuous )
proof end;

theorem Th22: :: JGRAPH_3:22
proof end;

registration
coherence by Th22;
end;

theorem Th23: :: JGRAPH_3:23
for Kb, Cb being Subset of () st Kb = { q where q is Point of () : ( ( - 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 () : |.p2.| = 1 } holds
Sq_Circ .: Kb = Cb
proof end;

theorem Th24: :: JGRAPH_3:24
for P, Kb being Subset of ()
for f being Function of (() | Kb),(() | P) st Kb = { q where q is Point of () : ( ( - 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 ) ) } & f is being_homeomorphism holds
P is being_simple_closed_curve
proof end;

theorem Th25: :: JGRAPH_3:25
for Kb being Subset of () st Kb = { q where q is Point of () : ( ( - 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 ) ) } holds
( Kb is being_simple_closed_curve & Kb is compact )
proof end;

theorem :: JGRAPH_3:26
for Cb being Subset of () st Cb = { p where p is Point of () : |.p.| = 1 } holds
Cb is being_simple_closed_curve
proof end;

theorem :: JGRAPH_3:27
for K0, C0 being Subset of () st K0 = { p where p is Point of () : ( - 1 <= p 1 & p 1 <= 1 & - 1 <= p 2 & p 2 <= 1 ) } & C0 = { p1 where p1 is Point of () : |.p1.| <= 1 } holds
Sq_Circ " C0 c= K0
proof end;

theorem Th28: :: JGRAPH_3:28
for p being Point of () holds
( ( p = 0. () implies () . p = 0. () ) & ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () implies () . 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 () . p = |[((p 1) * (sqrt (1 + (((p 1) / (p 2)) ^2)))),((p 2) * (sqrt (1 + (((p 1) / (p 2)) ^2))))]| ) )
proof end;

theorem Th29: :: JGRAPH_3:29
Sq_Circ " is Function of (),()
proof end;

theorem Th30: :: JGRAPH_3:30
for p being Point of () st p <> 0. () holds
( ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) implies () . p = |[((p 1) * (sqrt (1 + (((p 1) / (p 2)) ^2)))),((p 2) * (sqrt (1 + (((p 1) / (p 2)) ^2))))]| ) & ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) or () . p = |[((p 1) * (sqrt (1 + (((p 2) / (p 1)) ^2)))),((p 2) * (sqrt (1 + (((p 2) / (p 1)) ^2))))]| ) )
proof end;

theorem Th31: :: JGRAPH_3:31
for X being non empty TopSpace
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )
proof end;

theorem Th32: :: JGRAPH_3:32
for X being non empty TopSpace
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous & ( for q being Point of X holds f2 . q <> 0 ) holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r2 * (sqrt (1 + ((r1 / r2) ^2))) ) & g is continuous )
proof end;

theorem Th33: :: JGRAPH_3:33
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = (p 1) * (sqrt (1 + (((p 2) / (p 1)) ^2))) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 1 <> 0 ) holds
f is continuous
proof end;

theorem Th34: :: JGRAPH_3:34
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = (p 2) * (sqrt (1 + (((p 2) / (p 1)) ^2))) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 1 <> 0 ) holds
f is continuous
proof end;

theorem Th35: :: JGRAPH_3:35
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = (p 2) * (sqrt (1 + (((p 1) / (p 2)) ^2))) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 2 <> 0 ) holds
f is continuous
proof end;

theorem Th36: :: JGRAPH_3:36
for K1 being non empty Subset of ()
for f being Function of (() | K1),R^1 st ( for p being Point of () st p in the carrier of (() | K1) holds
f . p = (p 1) * (sqrt (1 + (((p 1) / (p 2)) ^2))) ) & ( for q being Point of () st q in the carrier of (() | K1) holds
q 2 <> 0 ) holds
f is continuous
proof end;

Lm17: for K1 being non empty Subset of () holds proj2 * (() | K1) is Function of (() | K1),R^1
proof end;

Lm18: for K1 being non empty Subset of () holds proj1 * (() | K1) is Function of (() | K1),R^1
proof end;

theorem Th37: :: JGRAPH_3:37
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th38: :: JGRAPH_3:38
for K0, B0 being Subset of ()
for f being Function of (() | K0),(() | B0) st f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) & p <> 0. () ) } holds
f is continuous
proof end;

theorem Th39: :: JGRAPH_3:39
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 2 <= p 1 & - (p 1) <= p 2 ) or ( p 2 >= p 1 & p 2 <= - (p 1) ) ) & p <> 0. () ) } holds
( f is continuous & K0 is closed )
proof end;

theorem Th40: :: JGRAPH_3:40
for B0 being Subset of ()
for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st f = () | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p 1 <= p 2 & - (p 2) <= p 1 ) or ( p 1 >= p 2 & p 1 <= - (p 2) ) ) & p <> 0. () ) } holds
( f is continuous & K0 is closed )
proof end;

theorem Th41: :: JGRAPH_3:41
for D being non empty Subset of () st D  = {(0. ())} holds
ex h being Function of (() | D),(() | D) st
( h = () | D & h is continuous )
proof end;

theorem Th42: :: JGRAPH_3:42
ex h being Function of (),() st
( h = Sq_Circ " & h is continuous )
proof end;

theorem Th43: :: JGRAPH_3:43
( Sq_Circ is Function of (),() & rng Sq_Circ = the carrier of () & ( for f being Function of (),() st f = Sq_Circ holds
f is being_homeomorphism ) )
proof end;

Lm19: now :: thesis: for pz2, pz1 being Real st (((pz2 ^2) + (pz1 ^2)) - 1) * (pz2 ^2) <= pz1 ^2 holds
((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0
let pz2, pz1 be Real; :: thesis: ( (((pz2 ^2) + (pz1 ^2)) - 1) * (pz2 ^2) <= pz1 ^2 implies ((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0 )
assume (((pz2 ^2) + (pz1 ^2)) - 1) * (pz2 ^2) <= pz1 ^2 ; :: thesis: ((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0
then (((pz2 ^2) * (pz2 ^2)) + ((pz2 ^2) * ((pz1 ^2) - 1))) - (pz1 ^2) <= (pz1 ^2) - (pz1 ^2) by XREAL_1:9;
hence ((pz2 ^2) - 1) * ((pz2 ^2) + (pz1 ^2)) <= 0 ; :: thesis: verum
end;

Lm20: now :: thesis: for px1 being Real holds
( not (px1 ^2) - 1 = 0 or px1 = 1 or px1 = - 1 )
let px1 be Real; :: thesis: ( not (px1 ^2) - 1 = 0 or px1 = 1 or px1 = - 1 )
assume (px1 ^2) - 1 = 0 ; :: thesis: ( px1 = 1 or px1 = - 1 )
then (px1 - 1) * (px1 + 1) = 0 ;
then ( px1 - 1 = 0 or px1 + 1 = 0 ) by XCMPLX_1:6;
hence ( px1 = 1 or px1 = - 1 ) ; :: thesis: verum
end;

theorem :: JGRAPH_3:44
for f, g being Function of I[01],()
for C0, KXP, KXN, KYP, KYN being Subset of ()
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of () : |.p.| <= 1 } & KXP = { q1 where q1 is Point of () : ( |.q1.| = 1 & q1 2 <= q1 1 & q1 2 >= - (q1 1) ) } & KXN = { q2 where q2 is Point of () : ( |.q2.| = 1 & q2 2 >= q2 1 & q2 2 <= - (q2 1) ) } & KYP = { q3 where q3 is Point of () : ( |.q3.| = 1 & q3 2 >= q3 1 & q3 2 >= - (q3 1) ) } & KYN = { q4 where q4 is Point of () : ( |.q4.| = 1 & q4 2 <= q4 1 & q4 2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
proof end;