=d & t1>=t2 & s1 in [.a,b.]
& s2 in [.a,b.] holds s1<=s2;
theorem :: JGRAPH_5:10
for n being Element of NAT holds -(0.TOP-REAL n)=0.TOP-REAL n;
begin :: Fashoda Meet Theorems for Circle in Special Case
theorem :: JGRAPH_5:11
for f,g being Function of I[01],TOP-REAL 2,a,b,c,d being Real, O
,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is
continuous one-to-one & a <> b & c <> d & (f.O)`1=a & c <=(f.O)`2 & (f.O)`2 <=d
& (f.I)`1=b & c <=(f.I)`2 & (f.I)`2 <=d & (g.O)`2=c & a <=(g.O)`1 & (g.O)`1 <=b
& (g.I)`2=d & a <=(g.I)`1 & (g.I)`1 <=b & (for r being Point of I[01] holds (a
>=(f.r)`1 or (f.r)`1>=b or c >=(f.r)`2 or (f.r)`2>=d) & (a >=(g.r)`1 or (g.r)`1
>=b or c >=(g.r)`2 or (g.r)`2>=d)) holds rng f meets rng g;
theorem :: JGRAPH_5:12
for f being Function of I[01],TOP-REAL 2 st f is continuous
one-to-one ex f2 being Function of I[01],TOP-REAL 2 st f2.0=f.1 & f2.1=f.0 &
rng f2=rng f & f2 is continuous & f2 is one-to-one;
reserve p,q for Point of TOP-REAL 2;
theorem :: JGRAPH_5:13
for f,g being Function of I[01],TOP-REAL 2, C0,KXP,KXN,KYP,KYN
being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is
continuous one-to-one & g is continuous one-to-one & C0={p: |.p.|<=1}& KXP={q1
where q1 is Point of TOP-REAL 2: |.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} & KXN={q2
where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3
where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4
where q4 is Point of TOP-REAL 2: |.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} & f.O in
KXN & f.I in KXP & g.O in KYP & g.I in KYN & rng f c= C0 & rng g c= C0 holds
rng f meets rng g;
theorem :: JGRAPH_5:14
for f,g being Function of I[01],TOP-REAL 2, C0,KXP,KXN,KYP,KYN
being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is
continuous one-to-one & g is continuous one-to-one & C0={p: |.p.|>=1}& KXP={q1
where q1 is Point of TOP-REAL 2: |.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} & KXN={q2
where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3
where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4
where q4 is Point of TOP-REAL 2: |.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;
theorem :: JGRAPH_5:15
for f,g being Function of I[01],TOP-REAL 2, C0,KXP,KXN,KYP,KYN
being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is
continuous one-to-one & g is continuous one-to-one & C0={p: |.p.|>=1}& KXP={q1
where q1 is Point of TOP-REAL 2: |.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} & KXN={q2
where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3
where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4
where q4 is Point of TOP-REAL 2: |.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} & f.O in
KXN & f.I in KXP & g.O in KYP & g.I in KYN & rng f c= C0 & rng g c= C0 holds
rng f meets rng g;
theorem :: JGRAPH_5:16
for f,g being Function of I[01],TOP-REAL 2, C0 being Subset of
TOP-REAL 2 st C0={q: |.q.|>=1} & f is continuous one-to-one & g is continuous
one-to-one & f.0=|[-1,0]| & f.1=|[1,0]| & g.1=|[0,1]| & g.0=|[0,-1]| & rng f c=
C0 & rng g c= C0 holds rng f meets rng g;
theorem :: JGRAPH_5:17
for p1,p2,p3,p4 being Point of TOP-REAL 2, C0 being Subset of TOP-REAL
2 st C0={p: |.p.|>=1} & |.p1.|=1 & |.p2.|=1 & |.p3.|=1 & |.p4.|=1 & (ex h being
Function of TOP-REAL 2,TOP-REAL 2 st h is being_homeomorphism & h.:C0 c= C0 & h
.p1=|[-1,0]| & h.p2=|[0,1]| & h.p3=|[1,0]| & h.p4=|[0,-1]|) holds for f,g being
Function of I[01],TOP-REAL 2 st f is continuous one-to-one & g is continuous
one-to-one & f.0=p1 & f.1=p3 & g.0=p4 & g.1=p2 & rng f c= C0 & rng g c= C0
holds rng f meets rng g;
begin :: Properties of Fan Morphisms
theorem :: JGRAPH_5:18
for cn being Real,q being Point of TOP-REAL 2 st -1