The abstract of the Mizar article:

General Fashoda Meet Theorem for Unit Circle and Square

by

Yatsuka Nakamura

Received February 25, 2003

MML identifier: JGRAPH_6

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, BOOLE, ABSVALUE, EUCLID, PRE_TOPC, SQUARE_1, RELAT_1,
      SUBSET_1, ARYTM_3, METRIC_1, RCOMP_1, FUNCT_5, TOPMETR, COMPTS_1,
      ORDINAL2, TOPS_2, ARYTM_1, ARYTM, COMPLEX1, MCART_1, PCOMPS_1, JGRAPH_3,
      BORSUK_1, TOPREAL1, TOPREAL2, JORDAN3, PSCOMP_1, REALSET1, JORDAN5C,
      JORDAN6, JGRAPH_2, JGRAPH_6, RELAT_2, FINSEQ_1, FINSEQ_4, TARSKI, TOPS_1,
      FUNCT_4, JORDAN17;
 notation XBOOLE_0, ORDINAL1, ABSVALUE, EUCLID, TARSKI, RELAT_1, TOPS_2,
      FUNCT_1, FUNCT_2, SUBSET_1, FINSEQ_1, STRUCT_0, TOPMETR, PCOMPS_1,
      COMPTS_1, METRIC_1, SQUARE_1, RCOMP_1, PRE_TOPC, FUNCT_4, JGRAPH_3,
      JORDAN5C, JORDAN6, TOPREAL2, CONNSP_1, FINSEQ_4, TOPS_1, JORDAN17,
      JGRAPH_2, NUMBERS, XCMPLX_0, XREAL_0, TOPRNS_1, TOPREAL1, PSCOMP_1,
      REAL_1, NAT_1;
 constructors TOPS_1, RCOMP_1, JGRAPH_2, TOPREAL2, TOPGRP_1, CONNSP_1,
      WELLFND1, JGRAPH_3, JORDAN5C, JORDAN6, TOPRNS_1, TREAL_1, FINSEQ_4,
      TOPS_2, JORDAN17, TOPREAL1, PSCOMP_1, REAL_1, NAT_1;
 clusters STRUCT_0, RELSET_1, FUNCT_1, EUCLID, PRE_TOPC, TOPMETR, SQUARE_1,
      PSCOMP_1, BORSUK_1, TOPREAL2, BORSUK_2, TOPREAL1, JGRAPH_3, TOPS_1,
      JGRAPH_2, TOPREAL6, XREAL_0, NAT_1, MEMBERED, XBOOLE_0;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;


begin :: Preliminaries

canceled;

theorem :: JGRAPH_6:2
for a,b,r being real number st 0<=r & r<=1 & a<=b holds
 a<=(1-r)*a+r*b & (1-r)*a+r*b<=b;

theorem :: JGRAPH_6:3
  for a,b being real number st a>=0 & b>0 or a>0 & b>=0 holds a+b>0;

theorem :: JGRAPH_6:4
for a,b being real number st -1<=a & a<=1 & -1<=b & b<=1
holds a^2*b^2<=1;

theorem :: JGRAPH_6:5
for a,b being real number st a>=0 & b>=0
holds a*sqrt(b)=sqrt(a^2*b);

theorem :: JGRAPH_6:6
for a,b being real number st -1<=a & a<=1 & -1<=b & b<=1
holds (-b)*sqrt(1+a^2)<=sqrt(1+b^2) & -sqrt(1+b^2)<= b*sqrt(1+a^2);

theorem :: JGRAPH_6:7
for a,b being real number st -1<=a & a<=1 & -1<=b & b<=1
holds b*sqrt(1+a^2)<=sqrt(1+b^2);

theorem :: JGRAPH_6:8
for a,b being real number st a>=b
holds a*sqrt(1+b^2)>= b*sqrt(1+a^2);

theorem :: JGRAPH_6:9
for a,c,d being real number,p being Point of TOP-REAL 2
st c <=d & p in LSeg(|[a,c]|,|[a,d]|) holds p`1=a & c <=p`2 & p`2<=d;

theorem :: JGRAPH_6:10
for a,c,d being real number,p being Point of TOP-REAL 2
st c <d & p`1=a & c <=p`2 & p`2<=d holds p in LSeg(|[a,c]|,|[a,d]|);

theorem :: JGRAPH_6:11
for a,b,d being real number,p being Point of TOP-REAL 2
st a <=b & p in LSeg(|[a,d]|,|[b,d]|) holds p`2=d & a <=p`1 & p`1<=b;

theorem :: JGRAPH_6:12  :: BORSUK_4:48
  for a,b being real number,B being Subset of I[01] st
   B=[.a,b.] holds B is closed;

theorem :: JGRAPH_6:13
for X being TopStruct,Y,Z being non empty TopStruct,
f being map of X,Y, g being map of X,Z holds dom f=dom g
& dom f=the carrier of X & dom f=[#]X;

theorem :: JGRAPH_6:14
for X being non empty TopSpace,B being non empty Subset of X
ex f being map of X|B,X st (for p being Point of X|B holds f.p=p) &
  f is continuous;

theorem :: JGRAPH_6:15
for X being non empty TopSpace,
f1 being map of X,R^1,a being real number st f1 is continuous
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=r1-a) & g is continuous;

theorem :: JGRAPH_6:16
for X being non empty TopSpace,
f1 being map of X,R^1,a being real number st f1 is continuous
holds ex g being map of X,R^1
st (for p being Point of X,r1 being real number st
f1.p=r1 holds g.p=a-r1) & g is continuous;

theorem :: JGRAPH_6:17
for X being non empty TopSpace, n being Nat,
p being Point of TOP-REAL n,
f being map of X,R^1 st f is continuous ex g being map of X,TOP-REAL n
st (for r being Point of X holds g.r=(f.r)*p) &
g is continuous;

theorem :: JGRAPH_6:18
Sq_Circ.(|[-1,0]|)= |[-1,0]|;

theorem :: JGRAPH_6:19
for P being compact non empty Subset of TOP-REAL 2
 st P={p where p is Point of TOP-REAL 2: |.p.|=1}
 holds Sq_Circ.(|[-1,0]|)=W-min(P);

theorem :: JGRAPH_6:20
for X being non empty TopSpace, n being Nat,
g1,g2 being map of X,TOP-REAL n st
g1 is continuous & g2 is continuous
ex g being map of X,TOP-REAL n st
(for r being Point of X holds g.r=g1.r + g2.r) &
g is continuous;

theorem :: JGRAPH_6:21
for X being non empty TopSpace, n being Nat,
p1,p2 being Point of TOP-REAL n,
f1,f2 being map of X,R^1 st
f1 is continuous & f2 is continuous
ex g being map of X,TOP-REAL n st
(for r being Point of X holds g.r=(f1.r)*p1+(f2.r)*p2) &
g is continuous;

theorem :: JGRAPH_6:22
  for f being Function,A being set st f is one-to-one & A c= dom f
   holds f".:(f.:A)=A;

begin

reserve p,p1,p2,p3,q,q1,q2 for Point of TOP-REAL 2,i,j for Nat,
        r,lambda for Real;

theorem :: JGRAPH_6:23
for f,g being map 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 KXP & f.I in KXN &
  g.O in KYP & g.I in KYN &
  rng f c= C0 & rng g c= C0
   holds rng f meets rng g;

theorem :: JGRAPH_6:24
for f,g being map 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 & f is one-to-one &
  g is continuous & g is 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 KXP & f.I in KXN &
  g.O in KYN & g.I in KYP &
  rng f c= C0 & rng g c= C0
   holds rng f meets rng g;

theorem :: JGRAPH_6:25
for p1,p2,p3,p4 being Point of TOP-REAL 2,
P being compact non empty Subset of TOP-REAL 2,C0 being Subset of TOP-REAL 2
 st P={p where p is Point of TOP-REAL 2: |.p.|=1}
 & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P
 holds
 (for f,g being map of I[01],TOP-REAL 2 st
  f is continuous one-to-one & g is continuous one-to-one &
  C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}&
  f.0=p3 & f.1=p1 & g.0=p2 & g.1=p4 &
  rng f c= C0 & rng g c= C0 holds rng f meets rng g);

theorem :: JGRAPH_6:26
for p1,p2,p3,p4 being Point of TOP-REAL 2,
P being compact non empty Subset of TOP-REAL 2,C0 being Subset of TOP-REAL 2
 st P={p where p is Point of TOP-REAL 2: |.p.|=1}
 & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P
 holds
 (for f,g being map of I[01],TOP-REAL 2 st
  f is continuous one-to-one & g is continuous one-to-one &
  C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}&
  f.0=p3 & f.1=p1 & g.0=p4 & g.1=p2 &
  rng f c= C0 & rng g c= C0 holds rng f meets rng g);

theorem :: JGRAPH_6:27
for p1,p2,p3,p4 being Point of TOP-REAL 2,
    P being compact non empty Subset of TOP-REAL 2,
    C0 being Subset of TOP-REAL 2 st
  P={p where p is Point of TOP-REAL 2: |.p.|=1} &
   p1,p2,p3,p4 are_in_this_order_on P holds
 (for f,g being map of I[01],TOP-REAL 2 st
  f is continuous one-to-one & g is continuous one-to-one &
  C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}&
  f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 &
  rng f c= C0 & rng g c= C0 holds rng f meets rng g);

begin :: General Rectangles and Circles

definition let a,b,c,d be real number;
  func rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 1
   {p: p`1=a & c <=p`2 & p`2<=d or p`2=d & a<=p`1 & p`1<=b or
      p`1=b & c <=p`2 & p`2<=d or p`2=c & a<=p`1 & p`1<=b};
end;

theorem :: JGRAPH_6:28
for a,b,c,d being real number, p being Point of TOP-REAL 2
 st a<=b & c <=d & p in rectangle(a,b,c,d) holds
  a<=p`1 & p`1<=b & c <=p`2 & p`2<=d;

 definition let a,b,c,d be real number;
  func inside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 2
   {p: a <p`1 & p`1< b & c <p`2 & p`2< d};
 end;

 definition let a,b,c,d be real number;
  func closed_inside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 3

   {p: a <=p`1 & p`1<= b & c <=p`2 & p`2<= d};
 end;

 definition let a,b,c,d be real number;
  func outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 4

   {p: not(a <=p`1 & p`1<= b & c <=p`2 & p`2<= d)};
 end;

 definition let a,b,c,d be real number;
  func closed_outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 5

   {p: not(a <p`1 & p`1< b & c <p`2 & p`2< d)};
 end;

theorem :: JGRAPH_6:29
for a,b,r being real number,Kb,Cb being Subset of TOP-REAL 2 st
 r>=0 & Kb={q: |.q.|=1}&
 Cb={p2 where p2 is Point of TOP-REAL 2: |.(p2- |[a,b]|).|=r} holds
 AffineMap(r,a,r,b).:Kb=Cb;

theorem :: JGRAPH_6:30
for P,Q being Subset of TOP-REAL 2 st
(ex f being map of (TOP-REAL 2)|P,(TOP-REAL 2)|Q st
f is_homeomorphism) & P is_simple_closed_curve holds
Q is_simple_closed_curve;

theorem :: JGRAPH_6:31
for P being Subset of TOP-REAL 2 st
  P is being_simple_closed_curve holds P is compact;

theorem :: JGRAPH_6:32
for a,b,r be real number, Cb being Subset of TOP-REAL 2 st r>0 &
  Cb={p where p is Point of TOP-REAL 2: |.(p- |[a,b]|).|=r}
 holds Cb is_simple_closed_curve;

 definition let a,b,r be real number;
  assume  r>0;
  func circle(a,b,r) -> compact non empty Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 6
   {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|=r};
 end;

definition let a,b,r be real number;
  func inside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 7
   {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|<r};
end;

definition let a,b,r be real number;
  func closed_inside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 8
   {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|<=r};
end;

definition let a,b,r be real number;
  func outside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 9
   {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|>r};
end;

definition let a,b,r be real number;
  func closed_outside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 10
   {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|>=r};
end;

theorem :: JGRAPH_6:33
for r being real number holds
 inside_of_circle(0,0,r)={p : |.p.|<r} &
 (r>0 implies circle(0,0,r)={p2 : |.p2.|=r}) &
 outside_of_circle(0,0,r)={p3 : |.p3.|>r} &
 closed_inside_of_circle(0,0,r)={q : |.q.|<=r} &
 closed_outside_of_circle(0,0,r)={q2 : |.q2.|>=r};

theorem :: JGRAPH_6:34
for Kb,Cb being Subset of TOP-REAL 2 st
 Kb={p: -1 <p`1 & p`1< 1 & -1 <p`2 & p`2< 1}&
 Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<1} holds Sq_Circ.:Kb=Cb;

theorem :: JGRAPH_6:35
for Kb,Cb being Subset of TOP-REAL 2 st
 Kb={p: not(-1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1)}&
 Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|>1} holds Sq_Circ.:Kb=Cb;

theorem :: JGRAPH_6:36
for Kb,Cb being Subset of TOP-REAL 2 st
 Kb={p: -1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1}&
 Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<=1} holds Sq_Circ.:Kb=Cb;

theorem :: JGRAPH_6:37
for Kb,Cb being Subset of TOP-REAL 2 st
 Kb={p: not(-1 <p`1 & p`1< 1 & -1 <p`2 & p`2< 1)}&
 Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|>=1} holds Sq_Circ.:Kb=Cb;

theorem :: JGRAPH_6:38
for P0,P1,P01,P11,K0,K1,K01,K11 being Subset of TOP-REAL 2,
P,K being non empty compact Subset of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
P= circle(0,0,1) &
P0= inside_of_circle(0,0,1) &
P1= outside_of_circle(0,0,1) &
P01= closed_inside_of_circle(0,0,1) &
P11= closed_outside_of_circle(0,0,1) &
K=rectangle(-1,1,-1,1) &
K0=inside_of_rectangle(-1,1,-1,1) &
K1=outside_of_rectangle(-1,1,-1,1) &
K01=closed_inside_of_rectangle(-1,1,-1,1) &
K11=closed_outside_of_rectangle(-1,1,-1,1) &
f=Sq_Circ
holds f.:K=P & f".:P=K & f.:K0=P0 & f".:P0=K0 & f.:K1=P1 & f".:P1=K1 &
f.:K01=P01 & f.:K11=P11 & f".:P01=K01 & f".:P11=K11;

begin :: Order of Points on Rectangle

theorem :: JGRAPH_6:39
  for a,b,c,d being real number st a <= b & c <= d holds
   LSeg(|[ a,c ]|, |[ a,d ]|) = { p1 : p1`1 = a & p1`2 <= d & p1`2 >= c}
 & LSeg(|[ a,d ]|, |[ b,d ]|) = { p2 : p2`1 <= b & p2`1 >= a & p2`2 = d}
 & LSeg(|[ a,c ]|, |[ b,c ]|) = { q1 : q1`1 <= b & q1`1 >= a & q1`2 = c}
 & LSeg(|[ b,c ]|, |[ b,d ]|) = { q2 : q2`1 = b & q2`2 <= d & q2`2 >= c};

theorem :: JGRAPH_6:40
for a,b,c,d being real number st a<=b & c <=d holds
 {p: p`1=a & c <=p`2 & p`2<=d or p`2=d & a<=p`1 & p`1<=b or
      p`1=b & c <=p`2 & p`2<=d or p`2=c & a<=p`1 & p`1<=b}
 = (LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|))
 \/ (LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|));

theorem :: JGRAPH_6:41
for a,b,c,d being real number st a <= b & c <= d holds
 LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,c]|,|[b,c]|) = {|[a,c]|};

theorem :: JGRAPH_6:42
for a,b,c,d being real number st a <= b & c <= d holds
 LSeg(|[a,c]|,|[b,c]|) /\ LSeg(|[b,c]|,|[b,d]|) = {|[b,c]|};

theorem :: JGRAPH_6:43
for a,b,c,d being real number st a <= b & c <= d holds
 LSeg(|[a,d]|,|[b,d]|) /\ LSeg(|[b,c]|,|[b,d]|) = {|[b,d]|};

theorem :: JGRAPH_6:44
for a,b,c,d being real number st a <= b & c <= d holds
 LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|) = {|[a,d]|};

theorem :: JGRAPH_6:45
 {q: -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}
 = {p: p`1=-1 & -1 <=p`2 & p`2<=1 or p`2=1 & -1<=p`1 & p`1<=1 or
      p`1=1 & -1 <=p`2 & p`2<=1 or p`2=-1 & -1<=p`1 & p`1<=1};

theorem :: JGRAPH_6:46
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds W-bound K = a;

theorem :: JGRAPH_6:47
 for K being non empty compact Subset of TOP-REAL 2,
 a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds N-bound K = d;

theorem :: JGRAPH_6:48
 for K being non empty compact Subset of TOP-REAL 2,
 a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds E-bound K = b;

theorem :: JGRAPH_6:49
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds S-bound K = c;

theorem :: JGRAPH_6:50
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds
 NW-corner K = |[a,d]|;

theorem :: JGRAPH_6:51
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds
 NE-corner K = |[b,d]|;

theorem :: JGRAPH_6:52
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds
 SW-corner K = |[a,c]|;

theorem :: JGRAPH_6:53
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds
 SE-corner K = |[b,c]|;

theorem :: JGRAPH_6:54
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
 holds W-most K = LSeg(|[a,c]|,|[a,d]|);

theorem :: JGRAPH_6:55
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
 holds E-most K = LSeg(|[b,c]|,|[b,d]|);

theorem :: JGRAPH_6:56
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<=b & c <=d
holds W-min K=|[a,c]| & E-max K=|[b,d]|;

theorem :: JGRAPH_6:57
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<b & c <d
holds LSeg(|[a,c]|,|[a,d]|) \/ LSeg(|[a,d]|,|[b,d]|)
 is_an_arc_of W-min(K),E-max(K)
 &
 LSeg(|[a,c]|,|[b,c]|) \/ LSeg(|[b,c]|,|[b,d]|)
 is_an_arc_of E-max(K),W-min(K);

theorem :: JGRAPH_6:58
for P,P1,P2 being Subset of TOP-REAL 2,
a,b,c,d being real number,
f1,f2 being FinSequence of TOP-REAL 2,
p0,p1,p01,p10 being Point of TOP-REAL 2 st
 a < b & c < d &
P={p: p`1=a & c <=p`2 & p`2<=d or p`2=d & a<=p`1 & p`1<=b or
      p`1=b & c <=p`2 & p`2<=d or p`2=c & a<=p`1 & p`1<=b} &
p0=|[a,c]| & p1=|[b,d]| & p01=|[a,d]| & p10=|[b,c]|
& f1=<*p0,p01,p1*>
& f2=<*p0,p10,p1*> holds
  f1 is_S-Seq &
  L~f1 = LSeg(p0,p01) \/ LSeg(p01,p1) &
  f2 is_S-Seq &
  L~f2 = LSeg(p0,p10) \/ LSeg(p10,p1) &
  P = L~f1 \/ L~f2 &
  L~f1 /\ L~f2 = {p0,p1} & f1/.1 = p0 &
  f1/.len f1=p1 & f2/.1 = p0 & f2/.len f2 = p1;

theorem :: JGRAPH_6:59
for P,P1,P2 being Subset of TOP-REAL 2,
a,b,c,d being real number,
f1,f2 being FinSequence of TOP-REAL 2,p1,p2 being Point of TOP-REAL 2 st
 a < b & c < d &
P={p: p`1=a & c <=p`2 & p`2<=d or p`2=d & a<=p`1 & p`1<=b or
      p`1=b & c <=p`2 & p`2<=d or p`2=c & a<=p`1 & p`1<=b} &
p1=|[a,c]| & p2=|[b,d]|
& f1=<*|[a,c]|,|[a,d]|,|[b,d]|*>
& f2=<*|[a,c]|,|[b,c]|,|[b,d]|*>
& P1=L~f1
& P2=L~f2
holds P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2
& P1 is non empty & P2 is non empty & P = P1 \/ P2 & P1 /\ P2 = {p1,p2};

theorem :: JGRAPH_6:60
for a,b,c,d being real number st
a < b & c < d
holds rectangle(a,b,c,d) is_simple_closed_curve;

theorem :: JGRAPH_6:61
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<b & c <d
holds Upper_Arc(K)= LSeg(|[a,c]|,|[a,d]|) \/ LSeg(|[a,d]|,|[b,d]|);

theorem :: JGRAPH_6:62
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number st K=rectangle(a,b,c,d) & a<b & c <d
holds Lower_Arc(K)= LSeg(|[a,c]|,|[b,c]|) \/ LSeg(|[b,c]|,|[b,d]|);

theorem :: JGRAPH_6:63
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
ex f being map of I[01],(TOP-REAL 2)|(Upper_Arc(K)) st f is_homeomorphism
& f.0=W-min(K) & f.1=E-max(K) & rng f=Upper_Arc(K) &
(for r being Real st r in [.0,1/2 .] holds
              f.r=(1-2*r)*|[a,c]|+(2*r)*|[a,d]|)&
(for r being Real st r in [.1/2,1 .] holds
    f.r=(1-(2*r-1))*|[a,d]|+(2*r-1)*|[b,d]|)&
(for p being Point of TOP-REAL 2 st p in LSeg(|[a,c]|,|[a,d]|)
  holds 0<=((p`2)-c)/(d-c)/2 & ((p`2)-c)/(d-c)/2<=1
        & f.(((p`2)-c)/(d-c)/2)=p)&
(for p being Point of TOP-REAL 2 st p in LSeg(|[a,d]|,|[b,d]|)
  holds 0<=((p`1)-a)/(b-a)/2 + 1/2 & ((p`1)-a)/(b-a)/2 + 1/2<=1
        & f.(((p`1)-a)/(b-a)/2 + 1/2)=p);

theorem :: JGRAPH_6:64
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
ex f being map of I[01],(TOP-REAL 2)|(Lower_Arc(K)) st f is_homeomorphism
& f.0=E-max(K) & f.1=W-min(K) & rng f=Lower_Arc(K) &
(for r being Real st r in [.0,1/2.] holds f.r=(1-2*r)*|[b,d]|+(2*r)*|[b,c]|)&
(for r being Real st r in [.1/2,1.] holds
    f.r=(1-(2*r-1))*|[b,c]|+(2*r-1)*|[a,c]|)&
(for p being Point of TOP-REAL 2 st p in LSeg(|[b,d]|,|[b,c]|)
  holds 0<=((p`2)-d)/(c-d)/2 & ((p`2)-d)/(c-d)/2<=1
        & f.(((p`2)-d)/(c-d)/2)=p)&
(for p being Point of TOP-REAL 2 st p in LSeg(|[b,c]|,|[a,c]|)
  holds 0<=((p`1)-b)/(a-b)/2+1/2 & ((p`1)-b)/(a-b)/2+1/2<=1
        & f.(((p`1)-b)/(a-b)/2+1/2)=p);

theorem :: JGRAPH_6:65
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
 & p1 in LSeg(|[a,c]|,|[a,d]|)
 & p2 in LSeg(|[a,c]|,|[a,d]|)
holds LE p1,p2,K iff p1`2<=p2`2;

theorem :: JGRAPH_6:66
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
 & p1 in LSeg(|[a,d]|,|[b,d]|)
 & p2 in LSeg(|[a,d]|,|[b,d]|)
holds LE p1,p2,K iff p1`1<=p2`1;

theorem :: JGRAPH_6:67
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
 & p1 in LSeg(|[b,c]|,|[b,d]|)
 & p2 in LSeg(|[b,c]|,|[b,d]|)
holds LE p1,p2,K iff p1`2>=p2`2;

theorem :: JGRAPH_6:68
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
 & p1 in LSeg(|[a,c]|,|[b,c]|)
 & p2 in LSeg(|[a,c]|,|[b,c]|)
holds LE p1,p2,K & p1<>W-min(K) iff p1`1>=p2`1 & p2<>W-min(K);

theorem :: JGRAPH_6:69
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
 & p1 in LSeg(|[a,c]|,|[a,d]|)
holds LE p1,p2,K iff p2 in LSeg(|[a,c]|,|[a,d]|) & p1`2<=p2`2
or p2 in LSeg(|[a,d]|,|[b,d]|) or p2 in LSeg(|[b,d]|,|[b,c]|)
or p2 in LSeg(|[b,c]|,|[a,c]|) & p2<>W-min(K);

theorem :: JGRAPH_6:70
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
 & p1 in LSeg(|[a,d]|,|[b,d]|)
holds LE p1,p2,K iff p2 in LSeg(|[a,d]|,|[b,d]|) & p1`1<=p2`1
or p2 in LSeg(|[b,d]|,|[b,c]|)
or p2 in LSeg(|[b,c]|,|[a,c]|) & p2<>W-min(K);

theorem :: JGRAPH_6:71
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c <d
 & p1 in LSeg(|[b,d]|,|[b,c]|)
holds LE p1,p2,K iff p2 in LSeg(|[b,d]|,|[b,c]|) & p1`2>=p2`2
or p2 in LSeg(|[b,c]|,|[a,c]|) & p2<>W-min(K);

theorem :: JGRAPH_6:72
for K being non empty compact Subset of TOP-REAL 2,
a,b,c,d being real number,p1,p2 being Point of TOP-REAL 2
 st K=rectangle(a,b,c,d) & a<b & c < d
 & p1 in LSeg(|[b,c]|,|[a,c]|)& p1<>W-min(K)
holds LE p1,p2,K iff p2 in LSeg(|[b,c]|,|[a,c]|) & p1`1>=p2`1 & p2<>W-min(K);

theorem :: JGRAPH_6:73
for x being set,a,b,c,d being real number
 st x in rectangle(a,b,c,d) & a<b & c <d
 holds x in LSeg(|[a,c]|,|[a,d]|) or x in LSeg(|[a,d]|,|[b,d]|)
 or x in LSeg(|[b,d]|,|[b,c]|) or x in LSeg(|[b,c]|,|[a,c]|);

begin :: General Fashoda Theorem for Unit Square

theorem :: JGRAPH_6:74
for p1,p2 being Point of TOP-REAL 2,
K being non empty compact Subset of TOP-REAL 2
st K=rectangle(-1,1,-1,1) & LE p1,p2,K &
p1 in LSeg(|[-1,-1]|,|[-1,1]|)
holds p2 in LSeg(|[-1,-1]|,|[-1,1]|)& p2`2>=p1`2 or
p2 in LSeg(|[-1,1]|,|[1,1]|) or p2 in LSeg(|[1,1]|,|[1,-1]|)
or p2 in LSeg(|[1,-1]|,|[-1,-1]|)& p2<>|[-1,-1]|;

theorem :: JGRAPH_6:75
for p1,p2 being Point of TOP-REAL 2,
P,K being non empty compact Subset of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
P= circle(0,0,1) & K=rectangle(-1,1,-1,1) & f=Sq_Circ
& p1 in LSeg(|[-1,-1]|,|[-1,1]|)& p1`2>=0 & LE p1,p2,K
holds LE f.p1,f.p2,P;

theorem :: JGRAPH_6:76
for p1,p2,p3 being Point of TOP-REAL 2,
P,K being non empty compact Subset of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
P= circle(0,0,1) & K=rectangle(-1,1,-1,1) & f=Sq_Circ
& p1 in LSeg(|[-1,-1]|,|[-1,1]|)& p1`2>=0 & LE p1,p2,K & LE p2,p3,K
holds LE f.p2,f.p3,P;

theorem :: JGRAPH_6:77
for p being Point of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
f=Sq_Circ & p`1=-1 & p`2<0 holds (f.p)`1<0 & (f.p)`2<0;

theorem :: JGRAPH_6:78
for p being Point of TOP-REAL 2,
P,K being non empty compact Subset of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
P= circle(0,0,1) & K=rectangle(-1,1,-1,1) & f=Sq_Circ
holds (f.p)`1>=0 iff p`1>=0;

theorem :: JGRAPH_6:79
for p being Point of TOP-REAL 2,
P,K being non empty compact Subset of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
P= circle(0,0,1) & K=rectangle(-1,1,-1,1) & f=Sq_Circ
holds (f.p)`2>=0 iff p`2>=0;

theorem :: JGRAPH_6:80
for p,q being Point of TOP-REAL 2,
 f being map of TOP-REAL 2,TOP-REAL 2 st
 f=Sq_Circ
 & p in LSeg(|[-1,-1]|,|[-1,1]|)
 & q in LSeg(|[1,-1]|,|[-1,-1]|) holds (f.p)`1<=(f.q)`1;

theorem :: JGRAPH_6:81
for p,q being Point of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
f=Sq_Circ & p in LSeg(|[-1,-1]|,|[-1,1]|) & q in LSeg(|[-1,-1]|,|[-1,1]|)
& p`2>=q`2 & p`2<0
holds (f.p)`2>=(f.q)`2;

theorem :: JGRAPH_6:82
for p1,p2,p3,p4 being Point of TOP-REAL 2,
P,K being non empty compact Subset of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
P= circle(0,0,1) & K=rectangle(-1,1,-1,1) & f=Sq_Circ
holds LE p1,p2,K & LE p2,p3,K & LE p3,p4,K implies
 f.p1,f.p2,f.p3,f.p4 are_in_this_order_on P;

theorem :: JGRAPH_6:83
for p1,p2 being Point of TOP-REAL 2,
P being non empty compact Subset of TOP-REAL 2 st
P is_simple_closed_curve & p1 in P & p2 in P & not LE p1,p2,P
holds LE p2,p1,P;

theorem :: JGRAPH_6:84
for p1,p2,p3 being Point of TOP-REAL 2,
P being non empty compact Subset of TOP-REAL 2 st
P is_simple_closed_curve & p1 in P & p2 in P & p3 in P holds
  LE p1,p2,P & LE p2,p3,P or LE p1,p3,P & LE p3,p2,P or
  LE p2,p1,P & LE p1,p3,P or LE p2,p3,P & LE p3,p1,P or
  LE p3,p1,P & LE p1,p2,P or LE p3,p2,P & LE p2,p1,P;

theorem :: JGRAPH_6:85
for p1,p2,p3 being Point of TOP-REAL 2,
P being non empty compact Subset of TOP-REAL 2 st
P is_simple_closed_curve & p1 in P & p2 in P & p3 in P &
LE p2,p3,P holds
LE p1,p2,P or LE p2,p1,P & LE p1,p3,P or LE p3,p1,P;

theorem :: JGRAPH_6:86
for p1,p2,p3,p4 being Point of TOP-REAL 2,
P being non empty compact Subset of TOP-REAL 2 st
P is_simple_closed_curve & p1 in P & p2 in P & p3 in P & p4 in P &
LE p2,p3,P & LE p3,p4,P holds
LE p1,p2,P or LE p2,p1,P & LE p1,p3,P or LE p3,p1,P & LE p1,p4,P or
LE p4,p1,P;

theorem :: JGRAPH_6:87
for p1,p2,p3,p4 being Point of TOP-REAL 2,
 P,K being non empty compact Subset of TOP-REAL 2,
 f being map of TOP-REAL 2,TOP-REAL 2 st
 P= circle(0,0,1) & K=rectangle(-1,1,-1,1) & f=Sq_Circ &
 LE f.p1,f.p2,P & LE f.p2,f.p3,P & LE f.p3,f.p4,P
 holds p1,p2,p3,p4 are_in_this_order_on K;

theorem :: JGRAPH_6:88
for p1,p2,p3,p4 being Point of TOP-REAL 2,
P,K being non empty compact Subset of TOP-REAL 2,
f being map of TOP-REAL 2,TOP-REAL 2 st
P= circle(0,0,1) & K=rectangle(-1,1,-1,1) & f=Sq_Circ
holds p1,p2,p3,p4 are_in_this_order_on K
  iff f.p1,f.p2,f.p3,f.p4 are_in_this_order_on P;

theorem :: JGRAPH_6:89
  for p1,p2,p3,p4 being Point of TOP-REAL 2,
K being compact non empty Subset of TOP-REAL 2,K0 being Subset of TOP-REAL 2
 st K=rectangle(-1,1,-1,1)
 & p1,p2,p3,p4 are_in_this_order_on K
 holds
 (for f,g being map of I[01],TOP-REAL 2 st
  f is continuous one-to-one & g is continuous one-to-one &
  K0= closed_inside_of_rectangle(-1,1,-1,1) &
  f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 &
  rng f c= K0 & rng g c= K0 holds rng f meets rng g);