:: General {F}ashoda Meet Theorem for Unit Circle and Square
::  by Yatsuka Nakamura
::
:: Received February 25, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XXREAL_0, CARD_1, RELAT_1, SQUARE_1, ARYTM_3, ARYTM_1,
      PRE_TOPC, EUCLID, RLTOPSP1, MCART_1, REAL_1, SUBSET_1, BORSUK_1,
      XXREAL_1, RCOMP_1, TOPMETR, STRUCT_0, XBOOLE_0, FUNCT_1, ORDINAL2,
      TARSKI, TOPS_1, METRIC_1, SUPINF_2, COMPLEX1, JGRAPH_3, PSCOMP_1,
      PCOMPS_1, JORDAN3, TOPS_2, JORDAN17, JGRAPH_2, TOPREAL2, TOPREAL1, SEQ_4,
      FINSEQ_1, PARTFUN1, NAT_1, JORDAN6, JORDAN5C, FUNCT_4, RELAT_2, JGRAPH_6;
 notations XBOOLE_0, ORDINAL1, XCMPLX_0, COMPLEX1, TARSKI, RELAT_1, TOPS_2,
      FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SUBSET_1, FINSEQ_1, FINSEQ_4,
      SEQ_4, STRUCT_0, TOPMETR, COMPTS_1, METRIC_1, SQUARE_1, RCOMP_1,
      PRE_TOPC, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, FUNCT_4, JGRAPH_3,
      JORDAN5C, JORDAN6, TOPREAL2, CONNSP_1, TOPS_1, JORDAN17, JGRAPH_2,
      NUMBERS, XREAL_0, TOPREAL1, PSCOMP_1, REAL_1, NAT_1, SPPOL_2, XXREAL_0;
 constructors FUNCT_4, REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, FINSEQ_4, TOPS_1,
      CONNSP_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, SPPOL_2, PSCOMP_1,
      JORDAN5C, JORDAN6, JGRAPH_2, JGRAPH_3, JORDAN17, PCOMPS_1, SEQ_4,
      FUNCSDOM, CONVEX1, BINOP_2;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
      SQUARE_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, EUCLID,
      TOPMETR, TOPREAL1, TOPREAL2, SPPOL_2, PSCOMP_1, JGRAPH_2, JGRAPH_3,
      XXREAL_2, COMPTS_1, RLTOPSP1, MEASURE6, FUNCT_1, VALUED_0, ORDINAL1;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;


begin

theorem :: JGRAPH_6:1
  for a,c,d being Real,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:2
  for a,c,d being Real,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:3
  for a,b,d being Real,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:4  :: BORSUK_4:48
  for a,b being Real,B being Subset of I[01] st
  B=[.a,b.] holds B is closed;

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

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

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

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

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

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

theorem :: JGRAPH_6:11
  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:12
  for X being non empty TopSpace, n being Nat,
  g1,g2 being Function of X,TOP-REAL n st g1 is continuous & g2 is continuous
  ex g being Function 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:13
  for X being non empty TopSpace, n being Nat,
  p1,p2 being Point of TOP-REAL n, f1,f2 being Function of X,R^1 st
  f1 is continuous & f2 is continuous ex g being Function of X,TOP-REAL n st
  (for r being Point of X holds g.r=(f1.r)*p1+(f2.r)*p2) & g is continuous;

begin

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

theorem :: JGRAPH_6: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 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: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 & 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:16
  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 Function 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:17
  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 Function 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:18
  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 Function 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

notation
  let a,b,c,d be Real;
  synonym rectangle(a,b,c,d) for [.a,b,c,d.];
end;

theorem :: JGRAPH_6:19
  for a,b,c,d being Real, 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;
  func inside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 1
  {p: a <p`1 & p`1< b & c <p`2 & p`2< d};
end;

definition
  let a,b,c,d be Real;
  func closed_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;
  func outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals
:: JGRAPH_6:def 3
  {p: not(a <=p`1 & p`1<= b & c <=p`2 & p`2<= d)};
end;

definition
  let a,b,c,d be Real;
  func closed_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;

theorem :: JGRAPH_6:20
  for a,b,r being Real,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:21
  for P,Q being Subset of TOP-REAL 2 st
  (ex f being Function of (TOP-REAL 2)|P,(TOP-REAL 2)|Q st
  f is being_homeomorphism) & P is being_simple_closed_curve holds
  Q is being_simple_closed_curve;

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

theorem :: JGRAPH_6:23
  for a,b,r be Real, 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 being_simple_closed_curve;

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

registration
  let a,b,r be Real;
  cluster circle(a,b,r) -> compact;
end;

registration
  let a,b be Real;
  let r be non negative Real;
  cluster circle(a,b,r) -> non empty;
end;

definition
  let a,b,r be Real;
  func inside_of_circle(a,b,r) -> 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;
  func closed_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;
  func outside_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;
  func closed_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;

theorem :: JGRAPH_6:24
  for r being Real 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:25
  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:26
  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:27
  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:28
  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:29
  for P0,P1,P01,P11,K0,K1,K01,K11 being Subset of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2,
  f being Function 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) &
  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.:rectangle(-1,1,-1,1)=P & f".:P=rectangle(-1,1,-1,1) &
  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:30
  for a,b,c,d being Real 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:31
  for a,b,c,d being Real st a <= b & c <= d holds
  LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,c]|,|[b,c]|) = {|[a,c]|};

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

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

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

theorem :: JGRAPH_6:35
  {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:36
  for a,b,c,d being Real st a<=b & c <=d
  holds W-bound rectangle(a,b,c,d) = a;

theorem :: JGRAPH_6:37
  for a,b,c,d being Real st a<=b & c <=d
  holds N-bound rectangle(a,b,c,d) = d;

theorem :: JGRAPH_6:38
  for a,b,c,d being Real st a<=b & c <=d
  holds E-bound rectangle(a,b,c,d) = b;

theorem :: JGRAPH_6:39
  for a,b,c,d being Real st a<=b & c <=d
  holds S-bound rectangle(a,b,c,d) = c;

theorem :: JGRAPH_6:40
  for a,b,c,d being Real st a<=b & c <=d holds
  NW-corner rectangle(a,b,c,d) = |[a,d]|;

theorem :: JGRAPH_6:41
  for a,b,c,d being Real st a<=b & c <=d holds
  NE-corner rectangle(a,b,c,d) = |[b,d]|;

theorem :: JGRAPH_6:42
  for a,b,c,d being Real st a<=b & c <=d
  holds SW-corner rectangle(a,b,c,d) = |[a,c]|;

theorem :: JGRAPH_6:43
  for a,b,c,d being Real st a<=b & c <=d
  holds SE-corner rectangle(a,b,c,d) = |[b,c]|;

theorem :: JGRAPH_6:44
  for a,b,c,d being Real st a<=b & c <=d
  holds W-most rectangle(a,b,c,d) = LSeg(|[a,c]|,|[a,d]|);

theorem :: JGRAPH_6:45
  for a,b,c,d being Real st a<=b & c <=d
  holds E-most rectangle(a,b,c,d) = LSeg(|[b,c]|,|[b,d]|);

theorem :: JGRAPH_6:46
  for a,b,c,d being Real st a<=b & c <=d
  holds W-min rectangle(a,b,c,d)=|[a,c]| & E-max rectangle(a,b,c,d)=|[b,d]|;

theorem :: JGRAPH_6:47
  for a,b,c,d being Real st a<b & c <d
  holds LSeg(|[a,c]|,|[a,d]|) \/ LSeg(|[a,d]|,|[b,d]|)
  is_an_arc_of W-min rectangle(a,b,c,d), E-max rectangle(a,b,c,d) &
  LSeg(|[a,c]|,|[b,c]|) \/ LSeg(|[b,c]|,|[b,d]|)
  is_an_arc_of E-max rectangle(a,b,c,d), W-min rectangle(a,b,c,d);

theorem :: JGRAPH_6:48
  for a,b,c,d being Real, f1,f2 being FinSequence of TOP-REAL 2,
  p0,p1,p01,p10 being Point of TOP-REAL 2 st a < b & c < d &
  p0=|[a,c]| & p1=|[b,d]| & p01=|[a,d]| & p10=|[b,c]| & f1=<*p0,p01,p1*>
  & f2=<*p0,p10,p1*> holds f1 is being_S-Seq &
  L~f1 = LSeg(p0,p01) \/ LSeg(p01,p1) &
  f2 is being_S-Seq & L~f2 = LSeg(p0,p10) \/ LSeg(p10,p1) &
  rectangle(a,b,c,d) = 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:49
  for P1,P2 being Subset of TOP-REAL 2, a,b,c,d being Real,
  f1,f2 being FinSequence of TOP-REAL 2,p1,p2 being Point of TOP-REAL 2 st
  a < b & c < d & 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 &
  rectangle(a,b,c,d) = P1 \/ P2 & P1 /\ P2 = {p1,p2};

theorem :: JGRAPH_6:50
  for a,b,c,d being Real st a < b & c < d
  holds rectangle(a,b,c,d) is being_simple_closed_curve;

theorem :: JGRAPH_6:51
  for a,b,c,d being Real st a<b & c <d holds
  Upper_Arc rectangle(a,b,c,d) = LSeg(|[a,c]|,|[a,d]|) \/ LSeg(|[a,d]|,|[b,d]|)
;

theorem :: JGRAPH_6:52
  for a,b,c,d being Real st a<b & c <d holds
  Lower_Arc rectangle(a,b,c,d)= LSeg(|[a,c]|,|[b,c]|) \/ LSeg(|[b,c]|,|[b,d]|);

theorem :: JGRAPH_6:53
  for a,b,c,d being Real st a<b & c <d
  ex f being Function of I[01],(TOP-REAL 2)|Upper_Arc rectangle(a,b,c,d)
  st f is being_homeomorphism
  & f.0=W-min rectangle(a,b,c,d) & f.1=E-max rectangle(a,b,c,d) &
  rng f=Upper_Arc rectangle(a,b,c,d) &
  (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:54
  for a,b,c,d being Real st a<b & c <d
  ex f being Function of I[01],(TOP-REAL 2)|(Lower_Arc rectangle(a,b,c,d))
  st f is being_homeomorphism
  & f.0=E-max rectangle(a,b,c,d) & f.1=W-min rectangle(a,b,c,d) &
  rng f=Lower_Arc rectangle(a,b,c,d) &
  (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:55
  for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st a<b & c <d
  & p1 in LSeg(|[a,c]|,|[a,d]|) & p2 in LSeg(|[a,c]|,|[a,d]|)
  holds LE p1,p2,rectangle(a,b,c,d) iff p1`2<=p2`2;

theorem :: JGRAPH_6:56
  for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2
  st a < b & c < d & p1 in LSeg(|[a,d]|,|[b,d]|) & p2 in LSeg(|[a,d]|,|[b,d]|)
  holds LE p1,p2,rectangle(a,b,c,d) iff p1`1<=p2`1;

theorem :: JGRAPH_6:57
  for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st a<b & c <d
  & p1 in LSeg(|[b,c]|,|[b,d]|) & p2 in LSeg(|[b,c]|,|[b,d]|)
  holds LE p1,p2,rectangle(a,b,c,d) iff p1`2>=p2`2;

theorem :: JGRAPH_6:58
  for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st a<b & c <d
  & p1 in LSeg(|[a,c]|,|[b,c]|) & p2 in LSeg(|[a,c]|,|[b,c]|)
  holds LE p1,p2,rectangle(a,b,c,d) &
  p1<>W-min rectangle(a,b,c,d) iff p1`1>=p2`1 & p2<>W-min rectangle(a,b,c,d);

theorem :: JGRAPH_6:59
  for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st a<b & c <d
  & p1 in LSeg(|[a,c]|,|[a,d]|)
holds LE p1,p2,rectangle(a,b,c,d) 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 rectangle(a,b,c,d);

theorem :: JGRAPH_6:60
  for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st a<b & c <d
  & p1 in LSeg(|[a,d]|,|[b,d]|)
holds LE p1,p2,rectangle(a,b,c,d) 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 rectangle(a,b,c,d);

theorem :: JGRAPH_6:61
  for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2
  st a<b & c <d & p1 in LSeg(|[b,d]|,|[b,c]|)
holds LE p1,p2,rectangle(a,b,c,d) iff p2 in LSeg(|[b,d]|,|[b,c]|) & p1`2>=p2`2
  or p2 in LSeg(|[b,c]|,|[a,c]|) & p2<>W-min rectangle(a,b,c,d);

theorem :: JGRAPH_6:62
  for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2
  st a<b & c < d & p1 in LSeg(|[b,c]|,|[a,c]|)& p1<>W-min rectangle(a,b,c,d)
  holds LE p1,p2,rectangle(a,b,c,d) iff p2 in LSeg(|[b,c]|,|[a,c]|) &
  p1`1>=p2`1 & p2<>W-min rectangle(a,b,c,d);

theorem :: JGRAPH_6:63
  for x being set,a,b,c,d being Real
  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:64
  for p1,p2 being Point of TOP-REAL 2
  st LE p1,p2,rectangle(-1,1,-1,1) & 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:65
  for p1,p2 being Point of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2,
  f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) & f=Sq_Circ
  & p1 in LSeg(|[-1,-1]|,|[-1,1]|)& p1`2>=0 & LE p1,p2,rectangle(-1,1,-1,1)
  holds LE f.p1,f.p2,P;

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

theorem :: JGRAPH_6:67
  for p being Point of TOP-REAL 2, f being Function 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:68
  for p being Point of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2,
  f being Function of TOP-REAL 2,TOP-REAL 2 st
  f=Sq_Circ
  holds (f.p)`1>=0 iff p`1>=0;

theorem :: JGRAPH_6:69
  for p being Point of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2,
  f being Function of TOP-REAL 2,TOP-REAL 2 st
  f=Sq_Circ
  holds (f.p)`2>=0 iff p`2>=0;

theorem :: JGRAPH_6:70
  for p,q being Point of TOP-REAL 2,
  f being Function 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:71
  for p,q being Point of TOP-REAL 2,
  f being Function 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:72
  for p1,p2,p3,p4 being Point of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2,
  f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) & f=Sq_Circ
  holds LE p1,p2,rectangle(-1,1,-1,1) & LE p2,p3,rectangle(-1,1,-1,1) &
  LE p3,p4,rectangle(-1,1,-1,1) implies
  f.p1,f.p2,f.p3,f.p4 are_in_this_order_on P;

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

theorem :: JGRAPH_6:74
  for p1,p2,p3 being Point of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2 st
  P is being_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:75
  for p1,p2,p3 being Point of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2 st
  P is being_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:76
  for p1,p2,p3,p4 being Point of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2 st
  P is being_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:77
  for p1,p2,p3,p4 being Point of TOP-REAL 2,
  P being non empty compact Subset of TOP-REAL 2,
  f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,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 rectangle(-1,1,-1,1);

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

theorem :: JGRAPH_6:79
  for p1,p2,p3,p4 being Point of TOP-REAL 2
  st p1,p2,p3,p4 are_in_this_order_on rectangle(-1,1,-1,1)
  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=p2 & g.1=p4 &
  rng f c= closed_inside_of_rectangle(-1,1,-1,1) &
  rng g c= closed_inside_of_rectangle(-1,1,-1,1)
  holds rng f meets rng g;