:: The {F}ashoda Meet Theorem for Continuous Mappings
::  by Yatsuka Nakamura , Andrzej Trybulec and Artur Korni{\l}owicz
::
:: Received September 14, 2005
:: Copyright (c) 2005-2019 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, SUBSET_1, PRE_TOPC, EUCLID, BORSUK_1, PCOMPS_1, TOPMETR,
      CARD_1, FINSEQ_1, XXREAL_0, ORDINAL4, FUNCT_1, ARYTM_3, RELAT_1,
      PARTFUN1, ORDINAL2, ARYTM_1, JGRAPH_6, CONVEX1, MCART_1, RLTOPSP1,
      REAL_1, TOPREALA, TARSKI, STRUCT_0, XXREAL_1, MEASURE5, XBOOLE_0,
      FCONT_2, METRIC_1, NAT_1, INT_1, COMPLEX1, XXREAL_2, RELAT_2, RCOMP_1,
      CONNSP_1, GRAPH_1, WEIERSTR, PSCOMP_1, GOBOARD1, GOBOARD4, TOPREAL1,
      BORSUK_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
      XREAL_0, COMPLEX1, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      FINSEQ_1, NAT_1, NAT_D, SEQM_3, STRUCT_0, TOPREAL1, PRE_TOPC, GOBOARD1,
      GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1, WEIERSTR, METRIC_1, TBSP_1,
      RCOMP_1, UNIFORM1, INT_1, CONNSP_1, PSCOMP_1, RLVECT_1, RLTOPSP1, EUCLID,
      BORSUK_1, BORSUK_2, JGRAPH_6, TOPREALA, TOPALG_2;
 constructors REAL_1, RCOMP_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL1, GOBOARD1,
      GOBOARD4, PSCOMP_1, WEIERSTR, UNIFORM1, JGRAPH_6, TOPALG_2, TOPREALA,
      BORSUK_2, NAT_D, XXREAL_2, FUNCSDOM, CONVEX1, BINOP_2, NUMBERS;
 registrations RELAT_1, XREAL_0, INT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, BORSUK_1,
      EUCLID, TOPREAL1, BORSUK_2, JORDAN5A, TOPALG_2, MEMBERED, VALUED_0,
      FUNCT_2, XXREAL_2, RELSET_1, SPPOL_1, TOPMETR, FUNCT_1, NAT_1, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, JORDAN1, TOPALG_2;
 equalities XBOOLE_0, RLTOPSP1, EUCLID, TOPREALA, STRUCT_0;
 expansions TARSKI, XBOOLE_0, TOPALG_2;
 theorems TARSKI, FUNCT_1, FINSEQ_1, NAT_1, FINSEQ_4, RELAT_1, FINSEQ_3,
      TOPREAL1, GOBOARD4, TOPREAL3, EUCLID, UNIFORM1, WEIERSTR, PRE_TOPC,
      TBSP_1, HEINE, COMPTS_1, TOPMETR, PSCOMP_1, BORSUK_1, RCOMP_1, FUNCT_2,
      XBOOLE_0, XBOOLE_1, TOPRNS_1, XCMPLX_1, JGRAPH_1, INT_1, XREAL_0,
      CONNSP_1, XREAL_1, BORSUK_2, TSEP_1, JGRAPH_6, JORDAN5B, FINSEQ_2,
      XXREAL_0, TOPS_2, PARTFUN1, XXREAL_1, XXREAL_2, SEQM_3, RLTOPSP1,
      RELSET_1, ORDINAL1;
 schemes FINSEQ_1, NAT_1;

begin

reserve x, y for set;
reserve i, j, n for Nat;
reserve p1, p2 for Point of TOP-REAL n;
reserve a, b, c, d for Real;

Lm1: I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by TOPMETR:20,def 7;

Lm2: for x being set,f being FinSequence st 1<=len f holds (f^<*x*>).1=f.1 & (
<*x*>^f).(len f +1)=f.len f
proof
  let x be set,f be FinSequence;
  assume
A1: 1<=len f;
  then
A2: len f in dom f by FINSEQ_3:25;
A3: (<*x*>^f).(len f +1)=(<*x*>^f).(len <*x*>+len f) by FINSEQ_1:39
    .=f.len f by A2,FINSEQ_1:def 7;
  1 in dom f by A1,FINSEQ_3:25;
  hence thesis by A3,FINSEQ_1:def 7;
end;

Lm3: for f being FinSequence of REAL st (for k being Nat st 1<=k &
k<len f holds f/.k<f/.(k+1)) holds f is increasing
proof
  let f be FinSequence of REAL;
  assume
A1: for k being Nat st 1<=k & k<len f holds f/.k<f/.(k+1);
  now
    let i,j;
    now
      defpred P[Nat] means i+(1+$1)<=len f implies f/.i<f/.(i+(1+$1
      ));
      assume that
A2:   i in dom f and
A3:   j in dom f and
A4:   i<j;
A5:   1<=i by A2,FINSEQ_3:25;
A6:   for k being Nat st P[k] holds P[(k+1)]
      proof
        let k be Nat;
        assume
A7:     i+(1+k)<=len f implies f/.i<f/.(i+(1+k));
        now
          1<=i+1 & i+1<=i+1+k by NAT_1:11;
          then
A8:       1<=i+1+k by XXREAL_0:2;
A9:       i+(1+(k+1))=i+(1+k)+1;
          1+k<1+(k+1) by NAT_1:13;
          then
A10:      i+(1+k)<i+(1+(k+1)) by XREAL_1:6;
          assume
A11:      i+(1+(k+1))<=len f;
          then i+(1+k)<len f by A10,XXREAL_0:2;
          then f/.(i+(1+k))<f/.(i+(1+(k+1))) by A1,A8,A9;
          hence f/.i<f/.(i+(1+(k+1))) by A7,A11,A10,XXREAL_0:2;
        end;
        hence thesis;
      end;
      i+1<=j by A4,NAT_1:13;
      then j-'(i+1)=j-(i+1) by XREAL_1:233;
      then
A12:  i+(1+(j-'(i+1))) = j;
A13:  f/.i=f.i by A2,PARTFUN1:def 6;
A14:  j<=len f by A3,FINSEQ_3:25;
      then i<len f by A4,XXREAL_0:2;
      then
A15:  P[0] by A1,A5;
      for k being Nat holds P[k] from NAT_1:sch 2(A15,A6);
      then f/.i<f/.j by A14,A12;
      hence f.i<f.j by A3,A13,PARTFUN1:def 6;
    end;
    hence i in dom f & j in dom f & i<j implies f.i<f.j;
  end;
  hence thesis by SEQM_3:def 1;
end;

registration
  let a, b, c, d;
  cluster closed_inside_of_rectangle(a,b,c,d) -> convex;
  coherence
  proof
    set P = closed_inside_of_rectangle(a,b,c,d);
A1: P = {p where p is Point of TOP-REAL 2: a <= p`1 & p`1 <= b & c <= p`2
    & p`2 <= d} by JGRAPH_6:def 2;
    let w1, w2 be Point of TOP-REAL 2;
    assume w1 in P & w2 in P;
    then
A2: ( ex p3 being Point of TOP-REAL 2 st p3 = w1 & a <= p3`1 & p3`1 <= b &
c <= p3 `2 & p3`2 <= d)& ex p4 being Point of TOP-REAL 2 st p4 = w2 & a <= p4`1
    & p4`1 <= b & c <= p4`2 & p4`2 <= d by A1;
    let x be object;
    assume x in LSeg(w1,w2);
    then consider l being Real such that
A3: x = (1-l)*w1 + l*w2 and
A4: 0 <= l & l <= 1;
    set w = (1-l)*w1 + l*w2;
A5: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A6: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
    then
A7: (l*w2)`2=l*w2`2 by EUCLID:52;
A8: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
    then ((1-l)*w1)`2= (1-l)*w1`2 by EUCLID:52;
    then w`2=(1-l)* w1`2+ l* w2`2 by A5,A7,EUCLID:52;
    then
A9: c <= w`2 & w`2 <= d by A2,A4,XREAL_1:173,174;
A10: (l*w2)`1=l*w2`1 by A6,EUCLID:52;
    ((1-l)*w1)`1= (1-l)*w1`1 by A8,EUCLID:52;
    then w`1=(1-l)* w1`1+ l* w2`1 by A5,A10,EUCLID:52;
    then a <= w`1 & w`1 <= b by A2,A4,XREAL_1:173,174;
    hence thesis by A1,A3,A9;
  end;
end;

registration
  let a, b, c, d;
  cluster Trectangle(a,b,c,d) -> convex;
  coherence
  by PRE_TOPC:8;
end;

theorem Th1:
  for e being positive Real, g being continuous Function
  of I[01],TOP-REAL n ex h being FinSequence of REAL st h.1=0 & h.len h=1 & 5<=
len h & rng h c= the carrier of I[01] & h is increasing &
   (for i being Nat,Q being Subset of I[01], W being Subset of Euclid n
    st 1<=i & i<len h &
  Q=[.h/.i,h/.(i+1).] & W=g.:(Q) holds diameter(W)<e)
proof
  1 in {r where r is Real:0<=r & r<=1};
  then
A1: 1 in [.0,1.] by RCOMP_1:def 1;
  {1} c= [.0,1.]
  by A1,TARSKI:def 1;
  then
A2: [.0,1.] \/ {1} =[.0,1.] by XBOOLE_1:12;
  Closed-Interval-TSpace(0,1) =TopSpaceMetr(Closed-Interval-MSpace(0,1))
  by TOPMETR:def 7;
  then
A3: the carrier of I[01] =the carrier of Closed-Interval-MSpace(0,1) by
TOPMETR:12,20
    .= [.0,1.] by TOPMETR:10;
  let e be positive Real, g be continuous Function of I[01],TOP-REAL
  n;
  reconsider e as positive Real;
A4:  n in NAT by ORDINAL1:def 12;
  then
  reconsider f=g as Function of Closed-Interval-MSpace(0,1),Euclid n by
    UNIFORM1:10;
A5: e/2<e by XREAL_1:216;
A6: e/2>0 by XREAL_1:215;
  f is uniformly_continuous by UNIFORM1:8,A4;
  then consider s1 being Real such that
A7: 0<s1 and
A8: for u1,u2 being Element of (Closed-Interval-MSpace(0,1)) st dist(u1,
  u2) < s1 holds dist((f/.u1),(f/.u2)) < e/2 by A6,UNIFORM1:def 1;
  set s=min(s1,1/2);
  defpred P[Nat,object] means $2=s/2*($1-1);
A9: 0<=s by A7,XXREAL_0:20;
  then reconsider j= [/ (2/s) \] as Nat by INT_1:53;
A10: 2/s<=j by INT_1:def 7;
A11: s<=s1 by XXREAL_0:17;
A12: for u1,u2 being Element of (Closed-Interval-MSpace(0,1)) st dist(u1,u2)
  < s holds dist((f/.u1),(f/.u2)) < e/2
  proof
    let u1,u2 be Element of (Closed-Interval-MSpace(0,1));
    assume dist(u1,u2) < s;
    then dist(u1,u2) < s1 by A11,XXREAL_0:2;
    hence thesis by A8;
  end;
A13: 2/s <= [/ (2/s) \] by INT_1:def 7;
  then 2/s-j<=0 by XREAL_1:47;
  then 1+(2/s-j)<=1+0 by XREAL_1:6;
  then
A14: s/2*(1+(2/s-j))<=s/2*1 by A9,XREAL_1:64;
A15: for k being Nat st k in Seg j ex x being object st P[k,x];
  consider p being FinSequence such that
A16: dom p = Seg j & for k being Nat st k in Seg j holds P[k,p.k] from
  FINSEQ_1:sch 1(A15);
A17: Seg len p=Seg j by A16,FINSEQ_1:def 3;
  rng (p^<*1*>) c= REAL
  proof
    let y be object;
A18: len (p^<*1*>)=len p+1 by FINSEQ_2:16;
    assume y in rng (p^<*1*>);
    then consider x being object such that
A19: x in dom (p^<*1*>) and
A20: y=(p^<*1*>).x by FUNCT_1:def 3;
    reconsider nx=x as Nat by A19;
A21: dom (p^<*1*>)=Seg len (p^<*1*>) by FINSEQ_1:def 3;
    then
A22: 1<=nx by A19,FINSEQ_1:1;
A23: 1<=nx by A19,A21,FINSEQ_1:1;
A24: nx<=len (p^<*1*>) by A19,A21,FINSEQ_1:1;
    per cases;
    suppose
      nx<len p+1;
      then
A25:  nx<=len p by NAT_1:13;
      then nx in Seg j by A17,A23,FINSEQ_1:1;
      then
A26:  p.nx=s/2*(nx-1) by A16;
      y=p.nx by A20,A22,A25,FINSEQ_1:64;
      hence thesis by A26,XREAL_0:def 1;
    end;
    suppose
      nx>=len p+1;
      then nx=len p+1 by A24,A18,XXREAL_0:1;
      then
A27:    y=1 by A20,FINSEQ_1:42;
       1 in REAL by XREAL_0:def 1;
      hence thesis by A27;
    end;
  end;
  then reconsider h1=p^<*1*> as FinSequence of REAL by FINSEQ_1:def 4;
A28: len h1 =len p+1 by FINSEQ_2:16;
  j in NAT by ORDINAL1:def 12;
  then
A29: len p=j by A16,FINSEQ_1:def 3;
A30: s<>0 by A7,XXREAL_0:15;
  then 2/s>=2/(1/2) by A9,XREAL_1:118,XXREAL_0:17;
  then 4<=j by A10,XXREAL_0:2;
  then
A31: 4+1<=len p+1 by A29,XREAL_1:6;
A32: s/2>0 by A9,A30,XREAL_1:215;
A33: for i being Nat,r1,r2 being Real st 1<=i & i<len p & r1=p.i
  & r2=p.(i+1) holds r1<r2 & r2-r1=s/2
  proof
    let i be Nat,r1,r2 be Real;
    assume that
A34: 1<=i & i<len p and
A35: r1=p.i and
A36: r2=p.(i+1);
    1<i+1 & i+1<=len p by A34,NAT_1:13;
    then (i+1) in Seg j by A17,FINSEQ_1:1;
    then
A37: r2=s/2*(i+1-1) by A16,A36;
    i<i+1 by NAT_1:13;
    then
A38: i-1<i+1-1 by XREAL_1:9;
A39: i in Seg j by A17,A34,FINSEQ_1:1;
    then r1=s/2*(i-1) by A16,A35;
    hence r1<r2 by A32,A37,A38,XREAL_1:68;
    r2-r1=s/2*(i)-s/2*(i-1) by A16,A35,A39,A37;
    hence thesis;
  end;
  0<s by A7,A30,XXREAL_0:20;
  then 0<j by A13,XREAL_1:139;
  then
A40: 0+1<=j by NAT_1:13;
  then 1 in Seg j by FINSEQ_1:1;
  then p.1=s/2*(1-1) by A16
    .=0;
  then
A41: h1.1=0 by A40,A29,Lm2;
  2*s<>0 by A7,XXREAL_0:15;
  then
A42: s/2*(2/s)=(2*s)/(2*s) & (2*s)/(2*s)=1 by XCMPLX_1:60,76;
  then
A43: 1-s/2*(j-1)=s/2*(1+(2/s- [/ (2/s) \]));
A44: for r1 being Real st r1=p.len p holds 1-r1<=s/2
  by A40,A29,FINSEQ_1:1,A14,A16,A43;
A45: for i being Nat st 1<=i & i<len h1 holds h1/.(i+1)-h1/.i<=s /2
  proof
    let i be Nat;
    assume that
A46: 1<=i and
A47: i<len h1;
A48: i+1<=len h1 by A47,NAT_1:13;
A49: i<=len p by A28,A47,NAT_1:13;
A50: 1<i+1 by A46,NAT_1:13;
    per cases;
    suppose
A51:  i<len p;
      then i+1<=len p by NAT_1:13;
      then
A52:  h1.(i+1)=p.(i+1) by A50,FINSEQ_1:64;
A53:  h1.i=p.i by A46,A51,FINSEQ_1:64;
      h1.i=h1/.i & h1.(i+1)=h1/.(i+1) by A46,A47,A48,A50,FINSEQ_4:15;
      hence thesis by A33,A46,A51,A53,A52;
    end;
    suppose
      i>=len p;
      then
A54:  i=len p by A49,XXREAL_0:1;
A55:  h1/.i=h1.i by A46,A47,FINSEQ_4:15
        .=p.i by A46,A49,FINSEQ_1:64;
      h1/.(i+1)=h1.(i+1) by A48,A50,FINSEQ_4:15
        .=1 by A54,FINSEQ_1:42;
      hence thesis by A44,A54,A55;
    end;
  end;
  [/ (2/s) \] < 2/s+1 by INT_1:def 7;
  then [/ (2/s) \] -1 < 2/s+1-1 by XREAL_1:9;
  then
A56: s/2*(j-1)<s/2*(2/s) by A32,XREAL_1:68;
A57: for i being Nat,r1 being Real st 1<=i & i<=len p & r1=p.i
  holds r1<1
  proof
    let i be Nat,r1 be Real;
    assume that
A58: 1<=i and
A59: i<=len p and
A60: r1=p.i;
    i-1<=j-1 by A29,A59,XREAL_1:9;
    then
A61: (s/2)*(i-1)<=(s/2)*(j-1) by A9,XREAL_1:64;
    i in Seg j by A17,A58,A59,FINSEQ_1:1;
    then r1=s/2*(i-1) by A16,A60;
    hence thesis by A56,A42,A61,XXREAL_0:2;
  end;
A62: for i being Nat st 1<=i & i<len h1 holds h1/.i<h1/.(i+1)
  proof
    let i be Nat;
    assume that
A63: 1<=i and
A64: i<len h1;
A65: i+1<=len h1 by A64,NAT_1:13;
A66: 1<i+1 by A63,NAT_1:13;
A67: i<=len p by A28,A64,NAT_1:13;
    per cases;
    suppose
A68:  i<len p;
      then i+1<=len p by NAT_1:13;
      then
A69:  h1.(i+1)=p.(i+1) by A66,FINSEQ_1:64;
A70:  h1.i=p.i by A63,A68,FINSEQ_1:64;
      h1.i=h1/.i & h1.(i+1)=h1/.(i+1) by A63,A64,A65,A66,FINSEQ_4:15;
      hence thesis by A33,A63,A68,A70,A69;
    end;
    suppose
      i>=len p;
      then
A71:  i=len p by A67,XXREAL_0:1;
A72:  h1/.(i+1)=h1.(i+1) by A65,A66,FINSEQ_4:15
        .=1 by A71,FINSEQ_1:42;
      h1/.i=h1.i by A63,A64,FINSEQ_4:15
        .=p.i by A63,A67,FINSEQ_1:64;
      hence thesis by A57,A63,A67,A72;
    end;
  end;
A73: dom g=the carrier of I[01] by FUNCT_2:def 1;
A74: for i being Nat,Q being Subset of I[01], W being Subset of
Euclid n st 1<=i & i<len h1 & Q=[.h1/.i,h1/.(i+1).] & W=g.:(Q) holds diameter(W
  )<e
  proof
    let i be Nat,Q be Subset of I[01], W be Subset of Euclid n;
    assume that
A75: 1<=i & i<len h1 and
A76: Q=[.h1/.i,h1/.(i+1).] and
A77: W=g.:(Q);
    h1/.i<h1/.(i+1) by A62,A75;
    then
A78: Q<>{} by A76,XXREAL_1:1;
A79: for x,y being Point of Euclid n st x in W & y in W holds dist(x,y)<= e/2
    proof
      let x,y be Point of Euclid n;
      assume that
A80:  x in W and
A81:  y in W;
      consider x3 being object such that
A82:  x3 in dom g and
A83:  x3 in Q and
A84:  x=g.x3 by A77,A80,FUNCT_1:def 6;
      reconsider x3 as Element of Closed-Interval-MSpace(0,1) by A82,Lm1,
TOPMETR:12;
      reconsider r3=x3 as Real by A83;
A85:  h1/.(i+1)-h1/.i<=s/2 by A45,A75;
      consider y3 being object such that
A86:  y3 in dom g and
A87:  y3 in Q and
A88:  y=g.y3 by A77,A81,FUNCT_1:def 6;
      reconsider y3 as Element of Closed-Interval-MSpace(0,1) by A86,Lm1,
TOPMETR:12;
      reconsider s3=y3 as Real by A87;
A89:  f.x3=(f/.x3) & f.y3=(f/.y3);
      |.r3-s3.|<=h1/.(i+1)-h1/.i by A76,A83,A87,UNIFORM1:12;
      then |.r3-s3.|<=s/2 by A85,XXREAL_0:2;
      then
A90:  dist(x3,y3)<=s/2 by HEINE:1;
      s/2<s by A9,A30,XREAL_1:216;
      then dist(x3,y3)<s by A90,XXREAL_0:2;
      hence thesis by A12,A84,A88,A89;
    end;
    then W is bounded by A6,TBSP_1:def 7;
    then diameter(W)<=e/2 by A73,A77,A78,A79,TBSP_1:def 8;
    hence thesis by A5,XXREAL_0:2;

  end;
A91: rng p c=[.0,1.]
  proof
    let y be object;
    assume y in rng p;
    then consider x being object such that
A92: x in dom p and
A93: y=p.x by FUNCT_1:def 3;
    reconsider nx=x as Nat by A92;
A94: p.nx=s/2*(nx-1) by A16,A92;
    then reconsider ry=p.nx as Real;
A95: x in Seg len p by A92,FINSEQ_1:def 3;
    then
A96: 1<=nx by FINSEQ_1:1;
    then
A97: nx-1>=1-1 by XREAL_1:9;
    nx<=len p by A95,FINSEQ_1:1;
    then ry<1 by A57,A96;
    then y in {rs where rs is Real:0<=rs & rs<=1} by A9,A93,A94,A97;
    hence thesis by RCOMP_1:def 1;
  end;
  rng <*1*> ={1} by FINSEQ_1:38;
  then rng h1 =rng p \/ {1} by FINSEQ_1:31;
  then
A98: rng h1 c=[.0,1.] \/ {1} by A91,XBOOLE_1:13;
  h1.len h1=1 by A28,FINSEQ_1:42;
  hence thesis by A28,A31,A41,A2,A98,A3,A62,A74,Lm3;
end;

theorem Th2:
  for P being Subset of TOP-REAL n st P c= LSeg(p1,p2) & p1 in P &
  p2 in P & P is connected holds P = LSeg(p1,p2)
proof
  let P be Subset of TOP-REAL n;
  assume that
A1: P c= LSeg(p1,p2) and
A2: p1 in P and
A3: p2 in P and
A4: P is connected;
  reconsider L=LSeg(p1,p2) as non empty Subset of TOP-REAL n by A1,A2;
  now
A5: the carrier of ((TOP-REAL n)|L)=[#]((TOP-REAL n)|L)
      .= L by PRE_TOPC:def 5;
    then reconsider PX=P as Subset of (TOP-REAL n)|L by A1;
    assume not LSeg(p1,p2) c= P;
    then consider x0 being object such that
A6: x0 in LSeg(p1,p2) and
A7: not x0 in P;
    reconsider p0=x0 as Point of TOP-REAL n by A6;
A8: LSeg(p0,p2)\{p0} c= LSeg(p0,p2) by XBOOLE_1:36;
A9: p1 in LSeg(p1,p2) by RLTOPSP1:68;
    then reconsider PX1=LSeg(p1,p0) as Subset of (TOP-REAL n)|L by A6,A5,
TOPREAL1:6;
A10: LSeg(p1,p0)\{p0} c= LSeg(p1,p0) by XBOOLE_1:36;
    LSeg(p1,p0) c= L by A6,A9,TOPREAL1:6;
    then reconsider R1=LSeg(p1,p0)\{p0} as Subset of (TOP-REAL n)|L by A10,A5,
XBOOLE_1:1;
A11: (TOP-REAL n)|L is T_2 by TOPMETR:2;
A12: p2 in LSeg(p1,p2) by RLTOPSP1:68;
    then LSeg(p0,p2) c= L by A6,TOPREAL1:6;
    then reconsider R2=LSeg(p0,p2)\{p0} as Subset of (TOP-REAL n)|L by A5,A8,
XBOOLE_1:1;
    reconsider PX2=LSeg(p0,p2) as Subset of (TOP-REAL n)|L by A6,A5,A12,
TOPREAL1:6;
A13: PX1 /\ PX2 ={p0} by A6,TOPREAL1:8;
A14: R1 c= PX1 by XBOOLE_1:36;
A15: now
      assume P c= R1;
      then
A16:  p2 in R1 by A3;
      p2 in PX2 by RLTOPSP1:68;
      then p2 in PX1 /\ PX2 by A14,A16,XBOOLE_0:def 4;
      hence contradiction by A3,A7,A13,TARSKI:def 1;
    end;
A17: {p0} c= LSeg(p1,p0)
    proof
      let d be object;
      assume d in {p0};
      then d=p0 by TARSKI:def 1;
      hence thesis by RLTOPSP1:68;
    end;
A18: {p0} c= LSeg(p0,p2)
    proof
      let d be object;
      assume d in {p0};
      then d=p0 by TARSKI:def 1;
      hence thesis by RLTOPSP1:68;
    end;
    PX2 is compact by COMPTS_1:19;
    then PX2 is closed by A11,COMPTS_1:7;
    then
A19: Cl PX2 =PX2 by PRE_TOPC:22;
A20: Cl R2 c= Cl PX2 by PRE_TOPC:19,XBOOLE_1:36;
    R1 /\ PX2 = PX1 /\ PX2 \ {p0} by XBOOLE_1:49
      .= {} by A13,XBOOLE_1:37;
    then R1/\ (Cl R2)={} by A19,A20,XBOOLE_1:3,27;
    then
A21: R1 misses (Cl R2);
A22: PX1 /\ PX2 ={p0} by A6,TOPREAL1:8;
A23: R2 c= PX2 by XBOOLE_1:36;
A24: now
      assume P c= R2;
      then
A25:  p1 in R2 by A2;
      p1 in PX1 by RLTOPSP1:68;
      then p1 in PX1 /\ PX2 by A23,A25,XBOOLE_0:def 4;
      hence contradiction by A2,A7,A13,TARSKI:def 1;
    end;
    PX1 is compact by COMPTS_1:19;
    then PX1 is closed by A11,COMPTS_1:7;
    then
A26: Cl PX1 =PX1 by PRE_TOPC:22;
A27: L=LSeg(p1,p0) \/ LSeg(p0,p2) by A6,TOPREAL1:5
      .=(LSeg(p1,p0)\{p0})\/{p0} \/ LSeg(p0,p2) by A17,XBOOLE_1:45
      .=(LSeg(p1,p0)\{p0})\/ ({p0} \/ LSeg(p0,p2)) by XBOOLE_1:4
      .= R1 \/ PX2 by A18,XBOOLE_1:12
      .= R1 \/ ((PX2 \{p0}) \/ {p0}) by A18,XBOOLE_1:45
      .= R1 \/ {p0} \/ R2 by XBOOLE_1:4;
A28: P c= R1 \/ R2
    proof
      let z be object;
      assume
A29:  z in P;
      then z in R1 \/ {p0} or z in R2 by A1,A27,XBOOLE_0:def 3;
      then z in R1 or z in {p0} or z in R2 by XBOOLE_0:def 3;
      hence thesis by A7,A29,TARSKI:def 1,XBOOLE_0:def 3;
    end;
A30: Cl R1 c= Cl PX1 by PRE_TOPC:19,XBOOLE_1:36;
    PX1 /\ R2 =PX1 /\ PX2 \ {p0} by XBOOLE_1:49
      .= {} by A22,XBOOLE_1:37;
    then (Cl R1) /\ R2={} by A26,A30,XBOOLE_1:3,27;
    then (Cl R1) misses R2;
    then
A31: R1,R2 are_separated by A21,CONNSP_1:def 1;
    PX is connected by A4,CONNSP_1:46;
    hence contradiction by A31,A28,A15,A24,CONNSP_1:16;
  end;
  hence thesis by A1;
end;

theorem Th3:
  for g being Path of p1,p2 st rng g c= LSeg(p1,p2) holds rng g = LSeg(p1,p2)
proof
  let g be Path of p1,p2;
  assume
A1: rng g c= LSeg(p1,p2);
A2: p2=g.1 by BORSUK_2:def 4;
A3: p1=g.0 by BORSUK_2:def 4;
  now
A4: g.:([#]I[01]) c= rng g
    proof
      let y be object;
      assume y in g.:([#]I[01]);
      then ex x being object st x in dom g & x in [#]I[01] & y=g.x by
FUNCT_1:def 6;
      hence thesis by FUNCT_1:def 3;
    end;
    1 in the carrier of I[01] by BORSUK_1:43;
    then 1 in dom g by FUNCT_2:def 1;
    then
A5: p2 in g.:([#]I[01]) by A2,FUNCT_1:def 6;
    0 in the carrier of I[01] by BORSUK_1:43;
    then 0 in dom g by FUNCT_2:def 1;
    then
A6: p1 in g.:([#]I[01]) by A3,FUNCT_1:def 6;
    [#]I[01] is connected by CONNSP_1:27;
    then
A7: g.:([#]I[01]) is connected by TOPS_2:61;
    assume not LSeg(p1,p2) c= rng g;
    hence contradiction by A1,A7,A6,A5,A4,Th2,XBOOLE_1:1;
  end;
  hence thesis by A1;
end;

:: Goboard Theorem in continuous case

theorem Th4:
  for P, Q being non empty Subset of TOP-REAL 2, p1, p2, q1, q2
being Point of TOP-REAL 2, f being Path of p1,p2, g being Path of q1,q2 st rng
f = P & rng g = Q & (for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1
& p`1<= p2`1) & (for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p
`1<= p2`1) & (for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<=
q2`2) & (for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2
  ) holds P meets Q
proof
A1: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
A2: [#](I[01]) is compact by COMPTS_1:1;
  let P,Q be non empty Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL
  2, f be Path of p1,p2, g be Path of q1,q2;
  assume that
A3: rng f = P and
A4: rng g = Q and
A5: for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2 `1 and
A6: for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2 `1 and
A7: for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2 `2 and
A8: for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2 `2;
  TopSpaceMetr(Euclid 2) = the TopStruct of TOP-REAL 2 by EUCLID:def 8;
  then reconsider P9=P,Q9=Q as Subset of TopSpaceMetr(Euclid 2);
  set e=min_dist_min(P9,Q9)/5;
  f.:(the carrier of I[01])=rng f by RELSET_1:22;
  then P is compact by A3,A2,WEIERSTR:8;
  then
A9: P9 is compact by A1,COMPTS_1:23;
  g.:([#](I[01]))=rng g by RELSET_1:22;
  then Q is compact by A4,A2,WEIERSTR:8;
  then
A10: Q9 is compact by A1,COMPTS_1:23;
  assume
A11: P /\ Q= {};
  then P misses Q;
  then
A12: min_dist_min(P9,Q9)>0 by A10,A9,JGRAPH_1:38;
  then
A13: e>0/5 by XREAL_1:74;
  then consider h being FinSequence of REAL such that
A14: h.1=0 and
A15: h.len h=1 and
A16: 5<=len h and
A17: rng h c= the carrier of I[01] and
A18: h is increasing and
A19: for i being Nat,R being Subset of I[01], W being Subset
of Euclid 2 st 1<=i & i<len h & R=[.h/.i,h/.(i+1).] & W=f.:(R) holds diameter(W
  )<e by Th1;
  deffunc F(Nat)=f.(h.$1);
  ex h19 being FinSequence st len h19=len h & for i be Nat st i in dom
  h19 holds h19.i=F(i) from FINSEQ_1:sch 2;
  then consider h19 being FinSequence such that
A20: len h19=len h and
A21: for i be Nat st i in dom h19 holds h19.i=f.(h.i);
A22: 1<=len h by A16,XXREAL_0:2;
  then
A23: len h in dom h19 by A20,FINSEQ_3:25;
  rng h19 c= the carrier of TOP-REAL 2
  proof
    let y be object;
A24: dom f= the carrier of I[01] by FUNCT_2:def 1;
    assume y in rng h19;
    then consider x being object such that
A25: x in dom h19 and
A26: y=h19.x by FUNCT_1:def 3;
    reconsider i=x as Nat by A25;
    dom h19=Seg len h19 by FINSEQ_1:def 3;
    then i in dom h by A20,A25,FINSEQ_1:def 3;
    then
A27: h.i in rng h by FUNCT_1:def 3;
    h19.i=f.(h.i) by A21,A25;
    then h19.i in rng f by A17,A27,A24,FUNCT_1:def 3;
    hence thesis by A26;
  end;
  then reconsider h1=h19 as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A28: len h1>=1 by A16,A20,XXREAL_0:2;
  then
A29: h1.1=h1/.1 by FINSEQ_4:15;
A30: f.0 = p1 by BORSUK_2:def 4;
A31: for i st 1<=i & i+1<=len h1 holds |.h1/.i-h1/.(i+1).|<e
  proof
    reconsider Pa=P as Subset of TOP-REAL 2;
A32: dom f =the carrier of I[01] by FUNCT_2:def 1;
    reconsider W1=P as Subset of Euclid 2 by TOPREAL3:8;
    let i;
    assume that
A33: 1<=i and
A34: i+1<=len h1;
A35: 1<i+1 by A33,NAT_1:13;
    then
A36: h.(i+1)=h/.(i+1) by A20,A34,FINSEQ_4:15;
A37: i+1 in dom h19 by A34,A35,FINSEQ_3:25;
    then
A38: h19.(i+1)=f.(h.(i+1)) by A21;
    then
A39: h1/.(i+1)=f.(h.(i+1)) by A34,A35,FINSEQ_4:15;
    set r1=((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))+1;
    [#](I[01]) is compact & f.:(the carrier of I[01])=rng f by COMPTS_1:1
,RELSET_1:22;
    then
A40: Pa is compact by A3,WEIERSTR:8;
A41: for x,y being Point of Euclid 2 st x in W1 & y in W1 holds dist(x,y) <=r1
    proof
      let x,y be Point of Euclid 2;
      assume that
A42:  x in W1 and
A43:  y in W1;
      reconsider pw1=x,pw2=y as Point of TOP-REAL 2 by A42,A43;
A44:  S-bound Pa <= pw2`2 & pw2`2 <= N-bound Pa by A40,A43,PSCOMP_1:24;
      S-bound Pa <= pw1`2 & pw1`2 <= N-bound Pa by A40,A42,PSCOMP_1:24;
      then
A45:  |.pw1`2-pw2`2.|<=(N-bound Pa) - (S-bound Pa) by A44,JGRAPH_1:27;
A46:  ((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa)) <= ((
E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa)) +1 by XREAL_1:29;
A47:  W-bound Pa <= pw2`1 & pw2`1 <= E-bound Pa by A40,A43,PSCOMP_1:24;
      W-bound Pa <= pw1`1 & pw1`1 <= E-bound Pa by A40,A42,PSCOMP_1:24;
      then |.pw1`1-pw2`1.|<=(E-bound Pa) - (W-bound Pa) by A47,JGRAPH_1:27;
      then |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.| <=((E-bound Pa) - (W-bound Pa))+
      ((N-bound Pa) - (S-bound Pa)) by A45,XREAL_1:7;
      then
A48:  |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.|<=r1 by A46,XXREAL_0:2;
      dist(x,y)=|.pw1-pw2.| & |.pw1-pw2.|<=|.pw1`1-pw2`1.|+|.pw1`2-pw2
      `2.| by JGRAPH_1:28,32;
      hence thesis by A48,XXREAL_0:2;
    end;
    i+1 in dom h by A20,A34,A35,FINSEQ_3:25;
    then h.(i+1) in rng h by FUNCT_1:def 3;
    then h19.(i+1) in rng f by A17,A38,A32,FUNCT_1:def 3;
    then
A49: f.(h.(i+1)) is Element of TOP-REAL 2 by A21,A37;
A50: i<len h1 by A34,NAT_1:13;
    then
A51: h.i=h/.i by A20,A33,FINSEQ_4:15;
A52: i in dom h by A20,A33,A50,FINSEQ_3:25;
    then
A53: h.i in rng h by FUNCT_1:def 3;
A54: i+1 in dom h by A20,A34,A35,FINSEQ_3:25;
    then h.(i+1) in rng h by FUNCT_1:def 3;
    then reconsider R=[.h/.i,h/.(i+1).] as Subset of I[01] by A17,A53,A51,A36,
BORSUK_1:40,XXREAL_2:def 12;
A55: i in dom h19 by A33,A50,FINSEQ_3:25;
    then
A56: h19.i=f.(h.i) by A21;
    then h19.i in rng f by A17,A53,A32,FUNCT_1:def 3;
    then f.(h.i) is Element of TOP-REAL 2 by A21,A55;
    then reconsider w1=f.(h.i),w2=f.(h.(i+1)) as Point of Euclid 2 by A49,
TOPREAL3:8;
    i<i+1 by NAT_1:13;
    then
A57: h/.i <= h/.(i+1) by A18,A52,A51,A54,A36,SEQM_3:def 1;
    then h.i in R by A51,XXREAL_1:1;
    then
A58: w1 in f.:R by A32,FUNCT_1:def 6;
    0 in the carrier of I[01] by BORSUK_1:43;
    then
A59: f.0 in rng f by A32,FUNCT_1:def 3;
    then S-bound Pa <= p1`2 & p1`2 <= N-bound Pa by A3,A30,A40,PSCOMP_1:24;
    then (S-bound Pa)<=(N-bound Pa) by XXREAL_0:2;
    then
A60: 0<=((N-bound Pa) - (S-bound Pa)) by XREAL_1:48;
    W-bound Pa <= p1`1 & p1`1 <= E-bound Pa by A3,A30,A40,A59,PSCOMP_1:24;
    then (W-bound Pa)<=(E-bound Pa) by XXREAL_0:2;
    then 0<=((E-bound Pa) - (W-bound Pa)) by XREAL_1:48;
    then
A61: W1 is bounded by A60,A41,TBSP_1:def 7;
    h.(i+1) in R by A36,A57,XXREAL_1:1;
    then
A62: w2 in f.:R by A32,FUNCT_1:def 6;
    reconsider W=f.:R as Subset of Euclid 2 by TOPREAL3:8;
    dom f=[#](I[01]) by FUNCT_2:def 1;
    then P=f.:([.0,1.]) by A3,BORSUK_1:40,RELAT_1:113;
    then W is bounded by A61,BORSUK_1:40,RELAT_1:123,TBSP_1:14;
    then
A63: dist(w1,w2)<=diameter(W) by A58,A62,TBSP_1:def 8;
    diameter W<e by A19,A20,A33,A50;
    then
A64: dist(w1,w2)<e by A63,XXREAL_0:2;
    h1/.i=f.(h.i) by A33,A50,A56,FINSEQ_4:15;
    hence thesis by A39,A64,JGRAPH_1:28;
  end;
A65: for i st i in dom h1 holds q1`2<=(h1/.i)`2 & (h1/.i)`2<=q2`2
  proof
    let i;
    assume
A66: i in dom h1;
    then h1.i=f.(h.i) by A21;
    then
A67: h1/.i=f.(h.i) by A66,PARTFUN1:def 6;
    i in dom h by A20,A66,FINSEQ_3:29;
    then
A68: h.i in rng h by FUNCT_1:def 3;
    dom f =the carrier of I[01] by FUNCT_2:def 1;
    then h1/.i in rng f by A17,A67,A68,FUNCT_1:def 3;
    hence thesis by A3,A7;
  end;
  for i st i in dom (Y_axis h1) holds q1`2<=(Y_axis h1).i & (Y_axis h1).
  i<=q2`2
  proof
    let i;
    assume i in dom (Y_axis h1);
    then i in Seg len (Y_axis h1) by FINSEQ_1:def 3;
    then i in Seg len h1 by A28,JGRAPH_1:42;
    then
A69: i in dom h1 by FINSEQ_1:def 3;
    then (Y_axis h1).i = (h1/.i)`2 by JGRAPH_1:43;
    hence thesis by A65,A69;
  end;
  then
A70: Y_axis(h1) lies_between q1`2,q2`2 by GOBOARD4:def 2;
A71: f.1 = p2 by BORSUK_2:def 4;
A72: for i st i in dom h1 holds (h1/.1)`1<=(h1/.i)`1 & (h1/.i)`1<=(h1/.len
  h1)`1
  proof
    len h in dom h19 by A20,A28,FINSEQ_3:25;
    then h1.len h1=f.(h.len h) by A20,A21;
    then
A73: h1/.len h1=f.(h.len h) by A28,FINSEQ_4:15;
    1 in dom h19 by A28,FINSEQ_3:25;
    then h1.1=f.(h.1) by A21;
    then
A74: h1/.1=f.(h.1) by A28,FINSEQ_4:15;
    let i;
    assume
A75: i in dom h1;
    then h1.i=f.(h.i) by A21;
    then
A76: h1/.i=f.(h.i) by A75,PARTFUN1:def 6;
    i in dom h by A20,A75,FINSEQ_3:29;
    then
A77: h.i in rng h by FUNCT_1:def 3;
    dom f =the carrier of I[01] by FUNCT_2:def 1;
    then h1/.i in rng f by A17,A76,A77,FUNCT_1:def 3;
    hence thesis by A3,A5,A30,A71,A14,A15,A74,A73;
  end;
  for i st i in dom X_axis h1 holds (X_axis h1).1<=(X_axis h1).i & (
  X_axis h1).i<=(X_axis h1).len h1
  proof
    let i;
A78: (X_axis h1).1=(h1/.1)`1 & (X_axis h1).len h1=(h1/.len h1)`1 by A28,
JGRAPH_1:41;
    assume i in dom X_axis h1;
    then i in Seg len (X_axis h1) by FINSEQ_1:def 3;
    then i in Seg len h1 by A28,JGRAPH_1:41;
    then
A79: i in dom h1 by FINSEQ_1:def 3;
    then (X_axis h1).i = (h1/.i)`1 by JGRAPH_1:43;
    hence thesis by A72,A79,A78;
  end;
  then X_axis(h1) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) by
GOBOARD4:def 2;
  then consider f2 being FinSequence of TOP-REAL 2 such that
A80: f2 is special and
A81: f2.1=h1.1 and
A82: f2.len f2=h1.len h1 and
A83: len f2>=len h1 and
A84: X_axis(f2) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) &
  Y_axis(f2) lies_between q1`2,q2`2 and
A85: for j st j in dom f2 holds ex k being Nat st k in dom
  h1 & |.(f2/.j - h1/.k).|<e and
A86: for j st 1<=j & j+1<=len f2 holds |.f2/.j - f2/.(j+1).|<e by A13,A31,A28
,A70,JGRAPH_1:39;
A87: len f2>=1 by A28,A83,XXREAL_0:2;
  then
A88: f2.len f2=f2/.len f2 by FINSEQ_4:15;
  consider hb being FinSequence of REAL such that
A89: hb.1=0 and
A90: hb.len hb=1 and
A91: 5<=len hb and
A92: rng hb c= the carrier of I[01] and
A93: hb is increasing and
A94: for i being Nat,R being Subset of I[01], W being Subset
  of Euclid 2 st 1<=i & i<len hb & R=[.hb/.i,hb/.(i+1).] & W=g.:(R) holds
  diameter(W)<e by A13,Th1;
  deffunc F(Nat)=g.(hb.$1);
  ex h29 being FinSequence st len h29=len hb & for i be Nat st i in dom
  h29 holds h29.i=F(i) from FINSEQ_1:sch 2;
  then consider h29 being FinSequence such that
A95: len h29=len hb and
A96: for i be Nat st i in dom h29 holds h29.i=g.(hb.i);
  rng h29 c= the carrier of TOP-REAL 2
  proof
    let y be object;
A97: dom g = the carrier of I[01] by FUNCT_2:def 1;
    assume y in rng h29;
    then consider x being object such that
A98: x in dom h29 and
A99: y=h29.x by FUNCT_1:def 3;
    reconsider i=x as Nat by A98;
    dom h29=Seg len h29 by FINSEQ_1:def 3;
    then i in dom hb by A95,A98,FINSEQ_1:def 3;
    then
A100: hb.i in rng hb by FUNCT_1:def 3;
    h29.i=g.(hb.i) by A96,A98;
    then h29.i in rng g by A92,A100,A97,FUNCT_1:def 3;
    hence thesis by A99;
  end;
  then reconsider h2=h29 as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A101: len h2>=1 by A91,A95,XXREAL_0:2;
  1 in dom h19 by A20,A22,FINSEQ_3:25;
  then
A102: h1/.1=f.(h.1) by A21,A29;
A103: 0 in the carrier of I[01] by BORSUK_1:43;
  then 0 in dom f by FUNCT_2:def 1;
  then
A104: p1 in P9 by A3,A30,FUNCT_1:def 3;
A105: 1<=len hb by A91,XXREAL_0:2;
  then
A106: h2.len h2=h2/.len h2 by A95,FINSEQ_4:15;
A107: g.0 = q1 by BORSUK_2:def 4;
A108: for i st 1<=i & i+1<=len h2 holds |. (h2/.i)-(h2/.(i+1)) .|<e
  proof
    reconsider Qa=Q as Subset of TOP-REAL 2;
A109: dom g =the carrier of I[01] by FUNCT_2:def 1;
    reconsider W1=Q as Subset of Euclid 2 by TOPREAL3:8;
    let i;
    assume that
A110: 1<=i and
A111: i+1<=len h2;
A112: i<len h2 by A111,NAT_1:13;
    then
A113: hb.i=hb/.i by A95,A110,FINSEQ_4:15;
A114: 1<i+1 by A110,NAT_1:13;
    then i+1 in Seg len hb by A95,A111,FINSEQ_1:1;
    then i+1 in dom hb by FINSEQ_1:def 3;
    then
A115: hb.(i+1) in rng hb by FUNCT_1:def 3;
A116: i+1 in dom h29 by A111,A114,FINSEQ_3:25;
    then h29.(i+1)=g.(hb.(i+1)) by A96;
    then h29.(i+1) in rng g by A92,A109,A115,FUNCT_1:def 3;
    then
A117: g.(hb.(i+1)) is Element of TOP-REAL 2 by A96,A116;
    i in dom h29 by A110,A112,FINSEQ_3:25;
    then
A118: h29.i=g.(hb.i) by A96;
    [#](I[01]) is compact & g.:(the carrier of I[01])=rng g by COMPTS_1:1
,RELSET_1:22;
    then
A119: Qa is compact by A4,WEIERSTR:8;
    reconsider Qa as non empty Subset of TOP-REAL 2;
    set r1= ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))+1;
A120: hb.(i+1)=hb/.(i+1) by A95,A111,A114,FINSEQ_4:15;
A121: for x,y being Point of Euclid 2 st x in W1 & y in W1 holds dist(x,y) <=r1
    proof
      let x,y be Point of Euclid 2;
      assume that
A122: x in W1 and
A123: y in W1;
      reconsider pw1=x,pw2=y as Point of TOP-REAL 2 by A122,A123;
A124: S-bound Qa <= pw2`2 & pw2`2 <= N-bound Qa by A119,A123,PSCOMP_1:24;
      S-bound Qa <= pw1`2 & pw1`2 <= N-bound Qa by A119,A122,PSCOMP_1:24;
      then
A125: |.pw1`2-pw2`2.|<=(N-bound Qa) - (S-bound Qa) by A124,JGRAPH_1:27;
A126: ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa)) <= ((
E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa)) +1 by XREAL_1:29;
A127: W-bound Qa <= pw2`1 & pw2`1 <= E-bound Qa by A119,A123,PSCOMP_1:24;
      W-bound Qa <= pw1`1 & pw1`1 <= E-bound Qa by A119,A122,PSCOMP_1:24;
      then |.pw1`1-pw2`1.|<=(E-bound Qa) - (W-bound Qa) by A127,JGRAPH_1:27;
      then |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.| <=((E-bound Qa) - (W-bound Qa))+
      ((N-bound Qa) - (S-bound Qa)) by A125,XREAL_1:7;
      then
A128: |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.|<=r1 by A126,XXREAL_0:2;
      dist(x,y)=|.pw1-pw2.| & |.pw1-pw2.|<=|.pw1`1-pw2`1.|+|.pw1`2-
      pw2`2.| by JGRAPH_1:28,32;
      hence thesis by A128,XXREAL_0:2;
    end;
    0 in the carrier of I[01] by BORSUK_1:43;
    then
A129: g.0 in rng g by A109,FUNCT_1:def 3;
    then S-bound Qa <= q1`2 & q1`2 <= N-bound Qa by A4,A107,A119,PSCOMP_1:24;
    then (S-bound Qa)<=(N-bound Qa) by XXREAL_0:2;
    then
A130: 0<=((N-bound Qa) - (S-bound Qa)) by XREAL_1:48;
    i in Seg len hb by A95,A110,A112,FINSEQ_1:1;
    then
A131: i in dom hb by FINSEQ_1:def 3;
    then
A132: hb.i in rng hb by FUNCT_1:def 3;
    then h29.i in rng g by A92,A118,A109,FUNCT_1:def 3;
    then reconsider w1=g.(hb.i),w2=g.(hb.(i+1)) as Point of Euclid 2 by A118
,A117,TOPREAL3:8;
    i+1 in Seg len hb by A95,A111,A114,FINSEQ_1:1;
    then
A133: i+1 in dom hb by FINSEQ_1:def 3;
    then hb.(i+1) in rng hb by FUNCT_1:def 3;
    then reconsider
    R=[.hb/.i,hb/.(i+1).] as Subset of I[01] by A92,A132,A113,A120,BORSUK_1:40
,XXREAL_2:def 12;
    i<i+1 by NAT_1:13;
    then
A134: hb/.i <= hb/.(i+1) by A93,A131,A113,A133,A120,SEQM_3:def 1;
    then hb.i in R by A113,XXREAL_1:1;
    then
A135: w1 in g.:(R) by A109,FUNCT_1:def 6;
    W-bound Qa <= q1`1 & q1`1 <= E-bound Qa by A4,A107,A119,A129,PSCOMP_1:24;
    then (W-bound Qa)<=(E-bound Qa) by XXREAL_0:2;
    then 0<=((E-bound Qa) - (W-bound Qa)) by XREAL_1:48;
    then
A136: W1 is bounded by A130,A121,TBSP_1:def 7;
    hb.(i+1) in R by A120,A134,XXREAL_1:1;
    then
A137: w2 in g.:(R) by A109,FUNCT_1:def 6;
    reconsider W=g.:(R) as Subset of Euclid 2 by TOPREAL3:8;
    dom g=[#](I[01]) by FUNCT_2:def 1;
    then Q=g.:([.0,1.]) by A4,BORSUK_1:40,RELAT_1:113;
    then W is bounded by A136,BORSUK_1:40,RELAT_1:123,TBSP_1:14;
    then
A138: dist(w1,w2)<=diameter(W) by A135,A137,TBSP_1:def 8;
    diameter(W)<e by A94,A95,A110,A112;
    then
A139: dist(w1,w2)<e by A138,XXREAL_0:2;
    h2.(i+1)=h2/.(i+1) by A111,A114,FINSEQ_4:15;
    then
A140: h2/.(i+1)=g.(hb.(i+1)) by A96,A116;
    h2/.i=g.(hb.i) by A110,A112,A118,FINSEQ_4:15;
    hence thesis by A140,A139,JGRAPH_1:28;
  end;
A141: dom hb=Seg len hb by FINSEQ_1:def 3;
A142: for i st i in dom hb holds h2/.i=g.(hb.i)
  proof
    let i;
    assume
A143: i in dom hb;
    then i in dom h29 by A95,FINSEQ_3:29;
    then
A144: h2.i=g.(hb.i) by A96;
    1<=i & i<=len hb by A141,A143,FINSEQ_1:1;
    hence thesis by A95,A144,FINSEQ_4:15;
  end;
A145: for i st i in dom h2 holds p1`1<=(h2/.i)`1 & (h2/.i)`1<=p2`1
  proof
    let i;
    assume i in dom h2;
    then i in Seg len h2 by FINSEQ_1:def 3;
    then i in dom hb by A95,FINSEQ_1:def 3;
    then
A146: h2/.i=g.(hb.i) & hb.i in rng hb by A142,FUNCT_1:def 3;
    dom g =the carrier of I[01] by FUNCT_2:def 1;
    then h2/.i in rng g by A92,A146,FUNCT_1:def 3;
    hence thesis by A4,A6;
  end;
  for i st i in dom (X_axis(h2)) holds p1`1<= (X_axis(h2)).i & (X_axis(
  h2)).i<=p2`1
  proof
    let i;
    assume i in dom (X_axis(h2));
    then i in Seg len (X_axis(h2)) by FINSEQ_1:def 3;
    then i in Seg len h2 by A101,JGRAPH_1:41;
    then
A147: i in dom h2 by FINSEQ_1:def 3;
    then (X_axis(h2)).i = (h2/.i)`1 by JGRAPH_1:43;
    hence thesis by A145,A147;
  end;
  then
A148: X_axis(h2) lies_between p1`1, p2`1 by GOBOARD4:def 2;
A149: g.1 = q2 by BORSUK_2:def 4;
A150: for i st i in dom h2 holds (h2/.1)`2<=(h2/.i)`2 & (h2/.i)`2<=(h2/.len
  h2)`2
  proof
    let i;
    assume i in dom h2;
    then i in Seg len h2 by FINSEQ_1:def 3;
    then i in dom hb by A95,FINSEQ_1:def 3;
    then
A151: h2/.i=g.(hb.i) & hb.i in rng hb by A142,FUNCT_1:def 3;
    1 in Seg len hb by A95,A101,FINSEQ_1:1;
    then 1 in dom hb by FINSEQ_1:def 3;
    then
A152: h2/.1=g.(hb.1) by A142;
    len hb in Seg len hb by A95,A101,FINSEQ_1:1;
    then len hb in dom hb by FINSEQ_1:def 3;
    then
A153: h2/.len h2=g.(hb.len hb) by A95,A142;
    dom g =the carrier of I[01] by FUNCT_2:def 1;
    then h2/.i in rng g by A92,A151,FUNCT_1:def 3;
    hence thesis by A4,A8,A107,A149,A89,A90,A152,A153;
  end;
  for i st i in dom (Y_axis(h2)) holds (Y_axis(h2)).1<=(Y_axis(h2)).i &
  (Y_axis(h2)).i <=(Y_axis(h2)).(len h2)
  proof
    let i;
A154: (Y_axis(h2)).1=(h2/.1)`2 & (Y_axis(h2)).len h2=(h2/.len h2)`2 by A101,
JGRAPH_1:42;
    assume i in dom (Y_axis(h2));
    then i in Seg len (Y_axis(h2)) by FINSEQ_1:def 3;
    then i in Seg len h2 by A101,JGRAPH_1:42;
    then
A155: i in dom h2 by FINSEQ_1:def 3;
    then (Y_axis(h2)).i = (h2/.i)`2 by JGRAPH_1:43;
    hence thesis by A150,A155,A154;
  end;
  then Y_axis(h2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2) by
GOBOARD4:def 2;
  then consider g2 being FinSequence of TOP-REAL 2 such that
A156: g2 is special and
A157: g2.1=h2.1 and
A158: g2.len g2=h2.len h2 and
A159: len g2>=len h2 and
A160: Y_axis(g2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2) &
  X_axis(g2) lies_between p1`1,p2`1 and
A161: for j st j in dom g2 holds ex k being Nat st k in dom
  h2 & |.((g2/.j) - h2/.k).|<e and
A162: for j st 1<=j & j+1<=len g2 holds |.(g2/.j) - g2/.(j+1).|<e by A13,A101
,A148,A108,JGRAPH_1:40;
A163: len g2>=1 by A101,A159,XXREAL_0:2;
  then
A164: g2/.len g2=g2.len g2 by FINSEQ_4:15;
  1 in dom hb by A105,FINSEQ_3:25;
  then
A165: (h2/.1)=q1 by A107,A89,A142;
A166: h2.1=h2/.1 by A105,A95,FINSEQ_4:15;
A167: h1.len h1=h1/.len h1 by A28,FINSEQ_4:15;
  then
A168: X_axis(f2).len f2=(h1/.len h1)`1 by A82,A87,A88,JGRAPH_1:41
    .=X_axis(h1).len h1 by A28,JGRAPH_1:41;
  len h in dom h19 by A20,A28,FINSEQ_3:25;
  then (h1/.len h1)=p2 by A71,A15,A20,A21,A167;
  then
A169: X_axis(f2).len f2=p2`1 by A82,A87,A167,A88,JGRAPH_1:41;
  5<=len f2 by A16,A20,A83,XXREAL_0:2;
  then
A170: 2<=len f2 by XXREAL_0:2;
  0 in dom g by A103,FUNCT_2:def 1;
  then
A171: q1 in Q9 by A4,A107,FUNCT_1:def 3;
A172: f2.1=f2/.1 by A87,FINSEQ_4:15;
  g2.1=g2/.1 by A163,FINSEQ_4:15;
  then
A173: (Y_axis(g2)).1=(h2/.1)`2 by A157,A163,A166,JGRAPH_1:42
    .=(Y_axis(h2)).1 by A101,JGRAPH_1:42;
  g2/.1=g2.1 by A163,FINSEQ_4:15;
  then
A174: Y_axis(g2).1=q1`2 by A157,A163,A165,A166,JGRAPH_1:42;
  len hb in dom hb by A105,FINSEQ_3:25;
  then (g2.len g2)=q2 by A149,A90,A95,A142,A158,A106;
  then
A175: Y_axis(g2).len g2=q2`2 by A163,A164,JGRAPH_1:42;
  g2.len g2=g2/.len g2 by A163,FINSEQ_4:15;
  then
A176: Y_axis(g2).len g2=(h2/.len h2)`2 by A158,A163,A106,JGRAPH_1:42
    .=Y_axis(h2).len h2 by A101,JGRAPH_1:42;
  5<=len g2 by A91,A95,A159,XXREAL_0:2;
  then
A177: 2<=len g2 by XXREAL_0:2;
  1 in dom h19 by A28,FINSEQ_3:25;
  then h1.1=f.(h.1) by A21;
  then
A178: X_axis(f2).1=p1`1 by A30,A14,A81,A87,A172,JGRAPH_1:41;
A179: (X_axis f2).1=(h1/.1)`1 by A81,A87,A29,A172,JGRAPH_1:41
    .=(X_axis h1).1 by A28,JGRAPH_1:41;
  now
    per cases;
    case
A180: p1=p2;
      0 in the carrier of I[01] by BORSUK_1:43;
      then 0 in dom f by FUNCT_2:def 1;
      then
A181: p1 in P by A3,A30,FUNCT_1:3;
      0 in the carrier of I[01] by BORSUK_1:43;
      then
A182: 0 in dom g by FUNCT_2:def 1;
      then
A183: q1 in Q by A4,A107,FUNCT_1:3;
A184: for q being Point of TOP-REAL 2 st q in Q holds q`1=p1`1
      proof
        let q be Point of TOP-REAL 2;
        assume q in Q;
        then p1`1<=q`1 & q`1<= p2`1 by A6;
        hence thesis by A180,XXREAL_0:1;
      end;
A185: now
        assume
A186:   q1`2=q2`2;
        q1`2<=p1`2 & p1`2<=q2`2 by A7,A181;
        then
A187:   p1`2=q1`2 by A186,XXREAL_0:1;
        q1`1=p1`1 by A4,A107,A184,A182,FUNCT_1:3;
        then q1=p1 by A187,TOPREAL3:6;
        hence contradiction by A11,A183,A181,XBOOLE_0:def 4;
      end;
A188: p1 in LSeg(q1,q2)
      proof
        1 in the carrier of I[01] by BORSUK_1:43;
        then 1 in dom g by FUNCT_2:def 1;
        then g.1 in rng g by FUNCT_1:3;
        then p1`1<=q2`1 & q2`1<= p2`1 by A4,A6,A149;
        then
A189:   p1`1=q2`1 by A180,XXREAL_0:1;
        set ln=(p1`2-q1`2)/(q2`2-q1`2);
A190:   ln*q2`2=(p1`2-q1`2)*q2`2/(q2`2-q1`2) by XCMPLX_1:74
          .=(p1`2*q2`2-q1`2*q2`2)/(q2`2-q1`2);
A191:   q2`2-q1`2 <>0 by A185;
        then 1-ln=(q2`2-q1`2)/(q2`2-q1`2)-(p1`2-q1`2)/(q2`2-q1`2) by
XCMPLX_1:60
          .=((q2`2-q1`2)-(p1`2-q1`2))/(q2`2-q1`2) by XCMPLX_1:120
          .=(q2`2-p1`2)/(q2`2-q1`2);
        then
A192:   (1-ln)*q1`2=(q2`2-p1`2)*q1`2/(q2`2-q1`2) by XCMPLX_1:74
          .=(q2`2*q1`2-p1`2*q1`2)/(q2`2-q1`2);
        0 in the carrier of I[01] by BORSUK_1:43;
        then 0 in dom g by FUNCT_2:def 1;
        then q1 in Q by A4,A107,FUNCT_1:3;
        then p1`1<=q1`1 & q1`1<= p2`1 by A6;
        then
A193:   p1`1=q1`1 by A180,XXREAL_0:1;
        0 in the carrier of I[01] by BORSUK_1:43;
        then 0 in dom f by FUNCT_2:def 1;
        then
A194:   f.0 in rng f by FUNCT_1:3;
        then
A195:   q1`2<=p1`2 by A3,A7,A30;
A196:   ((1-ln)*q1+ln*q2)`1= ((1-ln)*q1)`1+(ln*q2)`1 by TOPREAL3:2
          .=(1-ln)*q1`1+(ln*q2)`1 by TOPREAL3:4
          .=(1-ln)*p1`1+(ln)*p1`1 by A193,A189,TOPREAL3:4
          .=p1`1;
        ((1-ln)*q1+ln*q2)`2=((1-ln)*q1)`2+(ln*q2)`2 by TOPREAL3:2
          .=(1-ln)*q1`2+(ln*q2)`2 by TOPREAL3:4
          .=(1-ln)*q1`2+ln*q2`2 by TOPREAL3:4
          .=((q2`2*q1`2-p1`2*q1`2)+(p1`2*q2`2-q1`2*q2`2))/ (q2`2-q1`2) by A192
,A190,XCMPLX_1:62
          .=p1`2*(q2`2-q1`2)/(q2`2-q1`2)
          .=p1`2*((q2`2-q1`2)/(q2`2-q1`2)) by XCMPLX_1:74
          .=p1`2*1 by A191,XCMPLX_1:60
          .=p1`2;
        then
A197:   (1-ln)*q1+ln*q2=p1 by A196,TOPREAL3:6;
A198:   p1`2<=q2`2 by A3,A7,A30,A194;
        then q2`2>=q1`2 by A195,XXREAL_0:2;
        then q2`2>q1`2 by A185,XXREAL_0:1;
        then
A199:   q2`2-q1`2>0 by XREAL_1:50;
        p1`2-q1`2<=q2`2-q1`2 by A198,XREAL_1:13;
        then ln<= (q2`2-q1`2)/(q2`2-q1`2) by A199,XREAL_1:72;
        then
A200:   ln <= 1 by A199,XCMPLX_1:60;
        p1`2-q1`2>=0 by A195,XREAL_1:48;
        hence thesis by A199,A200,A197;
      end;
      1 in the carrier of I[01] by BORSUK_1:43;
      then 1 in dom g by FUNCT_2:def 1;
      then
A201: q2 in Q by A4,A149,FUNCT_1:3;
      Q c= LSeg(q1,q2)
      proof
        p1`1<=q2`1 & q2`1<= p2`1 by A6,A201;
        then
A202:   p1`1=q2`1 by A180,XXREAL_0:1;
        p1`1<=q1`1 & q1`1<= p2`1 by A6,A183;
        then
A203:   p1`1=q1`1 by A180,XXREAL_0:1;
        let z be object;
        assume
A204:   z in Q;
        then reconsider qz=z as Point of TOP-REAL 2;
A205:   qz`2<=q2`2 by A8,A204;
        set ln=(qz`2-q1`2)/(q2`2-q1`2);
A206:   ln*q2`2=(qz`2-q1`2)*q2`2/(q2`2-q1`2) by XCMPLX_1:74
          .=(qz`2*q2`2-q1`2*q2`2)/(q2`2-q1`2);
A207:   q2`2-q1`2 <>0 by A185;
        then 1-ln=(q2`2-q1`2)/(q2`2-q1`2)-(qz`2-q1`2)/(q2`2-q1`2) by
XCMPLX_1:60
          .=((q2`2-q1`2)-(qz`2-q1`2))/(q2`2-q1`2) by XCMPLX_1:120
          .=(q2`2-qz`2)/(q2`2-q1`2);
        then
A208:   (1-ln)*q1`2=(q2`2-qz`2)*q1`2/(q2`2-q1`2) by XCMPLX_1:74
          .=(q2`2*q1`2-qz`2*q1`2)/(q2`2-q1`2);
A209:   ((1-ln)*q1+ln*q2)`2=((1-ln)*q1)`2+(ln*q2)`2 by TOPREAL3:2
          .=(1-ln)*q1`2+(ln*q2)`2 by TOPREAL3:4
          .=(1-ln)*q1`2+ln*q2`2 by TOPREAL3:4
          .=((q2`2*q1`2-qz`2*q1`2)+(qz`2*q2`2-q1`2*q2`2))/ (q2`2-q1`2) by A208
,A206,XCMPLX_1:62
          .=qz`2*(q2`2-q1`2)/(q2`2-q1`2)
          .=qz`2*((q2`2-q1`2)/(q2`2-q1`2)) by XCMPLX_1:74
          .=qz`2*1 by A207,XCMPLX_1:60
          .=qz`2;
A210:   p1`1<=qz`1 & qz`1<= p2`1 by A6,A204;
        ((1-ln)*q1+ln*q2)`1= ((1-ln)*q1)`1+(ln*q2)`1 by TOPREAL3:2
          .=(1-ln)*q1`1+(ln*q2)`1 by TOPREAL3:4
          .=(1-ln)*p1`1+(ln)*p1`1 by A203,A202,TOPREAL3:4
          .=qz`1 by A180,A210,XXREAL_0:1;
        then
A211:   (1-ln)*q1+ln*q2=qz by A209,TOPREAL3:6;
A212:   q1`2<=qz`2 by A8,A204;
        then q2`2>=q1`2 by A205,XXREAL_0:2;
        then q2`2>q1`2 by A185,XXREAL_0:1;
        then
A213:   q2`2-q1`2>0 by XREAL_1:50;
        qz`2-q1`2<=q2`2-q1`2 by A205,XREAL_1:13;
        then ln<= (q2`2-q1`2)/(q2`2-q1`2) by A213,XREAL_1:72;
        then
A214:   ln <= 1 by A213,XCMPLX_1:60;
        qz`2-q1`2>=0 by A212,XREAL_1:48;
        hence thesis by A213,A214,A211;
      end;
      then p1 in Q by A4,A188,Th3;
      hence contradiction by A104,A11,XBOOLE_0:def 4;
    end;
    case
A215: p1<>p2;
A216: 1<=len hb by A91,XXREAL_0:2;
      then 1 in dom hb by FINSEQ_3:25;
      then
A217: h2/.1=g.(hb.1) by A142;
A218: now
        0 in the carrier of I[01] by BORSUK_1:43;
        then 0 in dom g by FUNCT_2:def 1;
        then
A219:   q1 in Q by A4,A107,FUNCT_1:3;
        0 in the carrier of I[01] by BORSUK_1:43;
        then
A220:   0 in dom f by FUNCT_2:def 1;
        then
A221:   p1 in P by A3,A30,FUNCT_1:3;
        assume
A222:   q1=q2;
A223:   for p being Point of TOP-REAL 2 st p in P holds p`2=q1`2
        proof
          let p be Point of TOP-REAL 2;
          assume p in P;
          then q1`2<=p`2 & p`2<= q2`2 by A7;
          hence thesis by A222,XXREAL_0:1;
        end;
A224:   now
          assume
A225:     p1`1=p2`1;
          p1`1<=q1`1 & q1`1<=p2`1 by A6,A219;
          then
A226:     q1`1=p1`1 by A225,XXREAL_0:1;
          p1`2=q1`2 by A3,A30,A223,A220,FUNCT_1:3;
          then p1=q1 by A226,TOPREAL3:6;
          hence contradiction by A11,A221,A219,XBOOLE_0:def 4;
        end;
A227:   q1 in LSeg(p1,p2)
        proof
          1 in the carrier of I[01] by BORSUK_1:43;
          then 1 in dom f by FUNCT_2:def 1;
          then f.1 in rng f by FUNCT_1:3;
          then q1`2<=p2`2 & p2`2<= q2`2 by A3,A7,A71;
          then
A228:     q1`2=p2`2 by A222,XXREAL_0:1;
          set ln=(q1`1-p1`1)/(p2`1-p1`1);
A229:     ln*p2`1=(q1`1-p1`1)*p2`1/(p2`1-p1`1) by XCMPLX_1:74
            .=(q1`1*p2`1-p1`1*p2`1)/(p2`1-p1`1);
A230:     p2`1-p1`1 <>0 by A224;
          then 1-ln=(p2`1-p1`1)/(p2`1-p1`1)-(q1`1-p1`1)/(p2`1-p1`1) by
XCMPLX_1:60
            .=((p2`1-p1`1)-(q1`1-p1`1))/(p2`1-p1`1) by XCMPLX_1:120
            .=(p2`1-q1`1)/(p2`1-p1`1);
          then
A231:     (1-ln)*p1`1=(p2`1-q1`1)*p1`1/(p2`1-p1`1) by XCMPLX_1:74
            .=(p2`1*p1`1-q1`1*p1`1)/(p2`1-p1`1);
          0 in the carrier of I[01] by BORSUK_1:43;
          then 0 in dom f by FUNCT_2:def 1;
          then f.0 in rng f by FUNCT_1:3;
          then q1`2<=p1`2 & p1`2<= q2`2 by A3,A7,A30;
          then
A232:     q1`2=p1`2 by A222,XXREAL_0:1;
          0 in the carrier of I[01] by BORSUK_1:43;
          then 0 in dom g by FUNCT_2:def 1;
          then
A233:     g.0 in rng g by FUNCT_1:3;
          then
A234:     p1`1<=q1`1 by A4,A6,A107;
A235:     ((1-ln)*p1+ln*p2)`2= ((1-ln)*p1)`2+(ln*p2)`2 by TOPREAL3:2
            .=(1-ln)*p1`2+(ln*p2)`2 by TOPREAL3:4
            .=(1-ln)*q1`2+(ln)*q1`2 by A232,A228,TOPREAL3:4;
          ((1-ln)*p1+ln*p2)`1=((1-ln)*p1)`1+(ln*p2)`1 by TOPREAL3:2
            .=(1-ln)*p1`1+(ln*p2)`1 by TOPREAL3:4
            .=(1-ln)*p1`1+ln*p2`1 by TOPREAL3:4
            .=((p2`1*p1`1-q1`1*p1`1)+(q1`1*p2`1-p1`1*p2`1))/ (p2`1-p1`1) by
A231,A229,XCMPLX_1:62
            .=q1`1*(p2`1-p1`1)/(p2`1-p1`1)
            .=q1`1*((p2`1-p1`1)/(p2`1-p1`1)) by XCMPLX_1:74
            .=q1`1*1 by A230,XCMPLX_1:60;
          then
A236:     (1-ln)*p1+ln*p2=q1 by A235,TOPREAL3:6;
A237:     q1`1<=p2`1 by A4,A6,A107,A233;
          then p2`1>=p1`1 by A234,XXREAL_0:2;
          then p2`1>p1`1 by A224,XXREAL_0:1;
          then
A238:     p2`1-p1`1>0 by XREAL_1:50;
          q1`1-p1`1<=p2`1-p1`1 by A237,XREAL_1:13;
          then ln<= (p2`1-p1`1)/(p2`1-p1`1) by A238,XREAL_1:72;
          then
A239:     ln <= 1 by A238,XCMPLX_1:60;
          q1`1-p1`1>=0 by A234,XREAL_1:48;
          hence thesis by A238,A239,A236;
        end;
        1 in the carrier of I[01] by BORSUK_1:43;
        then 1 in dom f by FUNCT_2:def 1;
        then
A240:   p2 in P by A3,A71,FUNCT_1:3;
        P c= LSeg(p1,p2)
        proof
          q1`2<=p2`2 & p2`2<= q2`2 by A7,A240;
          then
A241:     q1`2=p2`2 by A222,XXREAL_0:1;
          q1`2<=p1`2 & p1`2<= q2`2 by A7,A221;
          then
A242:     q1`2=p1`2 by A222,XXREAL_0:1;
          let z be object;
          assume
A243:     z in P;
          then reconsider pz=z as Point of TOP-REAL 2;
A244:     pz`1<=p2`1 by A5,A243;
          set ln=(pz`1-p1`1)/(p2`1-p1`1);
A245:     ln*p2`1=(pz`1-p1`1)*p2`1/(p2`1-p1`1) by XCMPLX_1:74
            .=(pz`1*p2`1-p1`1*p2`1)/(p2`1-p1`1);
A246:     p2`1-p1`1 <>0 by A224;
          then 1-ln=(p2`1-p1`1)/(p2`1-p1`1)-(pz`1-p1`1)/(p2`1-p1`1) by
XCMPLX_1:60
            .=((p2`1-p1`1)-(pz`1-p1`1))/(p2`1-p1`1) by XCMPLX_1:120
            .=(p2`1-pz`1)/(p2`1-p1`1);
          then
A247:     (1-ln)*p1`1=(p2`1-pz`1)*p1`1/(p2`1-p1`1) by XCMPLX_1:74
            .=(p2`1*p1`1-pz`1*p1`1)/(p2`1-p1`1);
A248:     ((1-ln)*p1+ln*p2)`1=((1-ln)*p1)`1+(ln*p2)`1 by TOPREAL3:2
            .=(1-ln)*p1`1+(ln*p2)`1 by TOPREAL3:4
            .=(1-ln)*p1`1+ln*p2`1 by TOPREAL3:4
            .=((p2`1*p1`1-pz`1*p1`1)+(pz`1*p2`1-p1`1*p2`1))/ (p2`1-p1`1) by
A247,A245,XCMPLX_1:62
            .=pz`1*(p2`1-p1`1)/(p2`1-p1`1)
            .=pz`1*((p2`1-p1`1)/(p2`1-p1`1)) by XCMPLX_1:74
            .=pz`1*1 by A246,XCMPLX_1:60
            .=pz`1;
A249:     q1`2<=pz`2 & pz`2<= q2`2 by A7,A243;
          ((1-ln)*p1+ln*p2)`2= ((1-ln)*p1)`2+(ln*p2)`2 by TOPREAL3:2
            .=(1-ln)*p1`2+(ln*p2)`2 by TOPREAL3:4
            .=(1-ln)*q1`2+(ln)*q1`2 by A242,A241,TOPREAL3:4
            .=pz`2 by A222,A249,XXREAL_0:1;
          then
A250:     (1-ln)*p1+ln*p2=pz by A248,TOPREAL3:6;
A251:     p1`1<=pz`1 by A5,A243;
          then p2`1>=p1`1 by A244,XXREAL_0:2;
          then p2`1>p1`1 by A224,XXREAL_0:1;
          then
A252:     p2`1-p1`1>0 by XREAL_1:50;
          pz`1-p1`1<=p2`1-p1`1 by A244,XREAL_1:13;
          then ln<= (p2`1-p1`1)/(p2`1-p1`1) by A252,XREAL_1:72;
          then
A253:     ln <= 1 by A252,XCMPLX_1:60;
          pz`1-p1`1>=0 by A251,XREAL_1:48;
          hence thesis by A252,A253,A250;
        end;
        then q1 in P by A3,A227,Th3;
        hence contradiction by A171,A11,XBOOLE_0:def 4;
      end;
      len hb in dom hb by A216,FINSEQ_3:25;
      then
A254: g2.1<>g2.len g2 by A107,A149,A89,A90,A95,A142,A157,A158,A166,A106,A218
,A217;
      f2/.1<>f2/.len f2 by A30,A71,A14,A15,A20,A21,A81,A82,A29,A172,A88,A102
,A23,A215;
      then L~f2 meets L~g2 by A80,A84,A156,A160,A172,A88,A178,A169,A174,A175
,A179,A168,A173,A176,A170,A177,A254,JGRAPH_1:26;
      then consider s being object such that
A255: s in L~f2 and
A256: s in L~g2 by XBOOLE_0:3;
      reconsider ps=s as Point of TOP-REAL 2 by A255;
      ps in union{ LSeg(f2,i) : 1 <= i & i+1 <= len f2 } by A255,TOPREAL1:def 4
;
      then consider x such that
A257: ps in x & x in { LSeg(f2,i) : 1 <= i & i+1 <= len f2 } by TARSKI:def 4;
      ps in union{ LSeg(g2,j) : 1 <= j & j+1 <= len g2 } by A256,TOPREAL1:def 4
;
      then consider y such that
A258: ps in y & y in { LSeg(g2,j) : 1 <= j & j+1 <= len g2 } by TARSKI:def 4;
      consider i such that
A259: x=LSeg(f2,i) and
A260: 1 <= i and
A261: i+1 <= len f2 by A257;
      LSeg(f2,i)=LSeg(f2/.i,f2/.(i+1)) by A260,A261,TOPREAL1:def 3;
      then
A262: |.ps-f2/.i.|<=|.f2/.i-f2/.(i+1).| by A257,A259,JGRAPH_1:36;
      i<len f2 by A261,NAT_1:13;
      then i in dom f2 by A260,FINSEQ_3:25;
      then consider k being Nat such that
A263: k in dom h1 and
A264: |.f2/.i - h1/.k.|<e by A85;
      consider j such that
A265: y=LSeg(g2,j) and
A266: 1 <= j and
A267: j+1 <= len g2 by A258;
      LSeg(g2,j)=LSeg((g2/.j),g2/.(j+1)) by A266,A267,TOPREAL1:def 3;
      then
A268: |.ps-(g2/.j).|<=|.(g2/.j)-g2/.(j+1).| by A258,A265,JGRAPH_1:36;
      reconsider p11=h1/.k as Point of TOP-REAL 2;
      |.f2/.i-f2/.(i+1).|<e by A86,A260,A261;
      then |.ps-f2/.i.|<e by A262,XXREAL_0:2;
      then |.ps-h1/.k.|<=|.ps-f2/.i.|+|.f2/.i-h1/.k.| & |.ps-f2/.i.|+|.f2/.i-
      h1/.k.|<e+ e by A264,TOPRNS_1:34,XREAL_1:8;
      then |.ps-h1/.k.|<e+e by XXREAL_0:2;
      then
A269: |.(p11-ps).|<e+e by TOPRNS_1:27;
A270: k in Seg len h1 by A263,FINSEQ_1:def 3;
      then 1<=k & k<=len h1 by FINSEQ_1:1;
      then h1.k=h1/.k by FINSEQ_4:15;
      then
A271: h1/.k=f.(h.k) by A21,A263;
      j<len g2 by A267,NAT_1:13;
      then j in dom g2 by A266,FINSEQ_3:25;
      then consider k9 being Nat such that
A272: k9 in dom h2 and
A273: |.((g2/.j) - h2/.k9).|<e by A161;
      k9 in Seg len h2 by A272,FINSEQ_1:def 3;
      then k9 in dom hb by A95,FINSEQ_1:def 3;
      then
A274: hb.k9 in rng hb & h2/.k9=g.(hb.k9) by A142,FUNCT_1:def 3;
      reconsider q11=h2/.k9 as Point of TOP-REAL 2;
      reconsider x1=p11,x2=q11 as Point of Euclid 2 by EUCLID:22;
      dom g =the carrier of I[01] by FUNCT_2:def 1;
      then
A275: h2/.k9 in rng g by A92,A274,FUNCT_1:def 3;
      k in dom h by A20,A270,FINSEQ_1:def 3;
      then
A276: h.k in rng h by FUNCT_1:def 3;
      dom f=the carrier of I[01] by FUNCT_2:def 1;
      then h1/.k in P by A3,A17,A271,A276,FUNCT_1:def 3;
      then min_dist_min(P9,Q9)<=dist(x1,x2) by A4,A10,A9,A275,WEIERSTR:34;
      then
A277: min_dist_min(P9,Q9)<=|.(p11-q11).| by JGRAPH_1:28;
      |.(g2/.j)-g2/.(j+1).|<e by A162,A266,A267;
      then |.ps-(g2/.j).|<e by A268,XXREAL_0:2;
      then |.ps-h2/.k9.|<=|.ps-(g2/.j).|+|.(g2/.j)-h2/.k9.| & |.ps-(g2/.j).|+
      |.(g2/.j)- (h2/.k9).|<e+e by A273,TOPRNS_1:34,XREAL_1:8;
      then |.ps-(h2/.k9).|<e+e by XXREAL_0:2;
      then |.(p11-q11).|<= |.(p11-ps).|+|.(ps-q11).| & |.(p11-ps).|+|.(ps-q11
      ).| <e+e+( e+e) by A269,TOPRNS_1:34,XREAL_1:8;
      then |.(p11-q11).|<e+e+e+e by XXREAL_0:2;
      then min_dist_min(P9,Q9)<4*e by A277,XXREAL_0:2;
      then 4*e-5*e>0 by XREAL_1:50;
      then (4-5)*e/e>0 by A13,XREAL_1:139;
      then 4-5>0 by A12;
      hence contradiction;
    end;
  end;
  hence contradiction;
end;

:: Fashoda Meet Theorem

theorem Th5:
  for f,g being continuous Function of I[01],TOP-REAL 2, O,I being
Point of I[01] st O=0 & I=1 & (f.O)`1=a & (f.I)`1=b & (g.O)`2=c & (g.I)`2=d & (
for r being Point of I[01] holds a <=(f.r)`1 & (f.r)`1<=b & a <=(g.r)`1 & (g.r)
`1<=b & c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d) holds rng f meets
  rng g
proof
  let f,g be continuous Function of I[01],TOP-REAL 2, O,I be Point of I[01];
  assume that
A1: O=0 & I=1 and
A2: (f.O)`1=a and
A3: (f.I)`1=b and
A4: (g.O)`2=c and
A5: (g.I)`2=d and
A6: for r being Point of I[01] holds a<=(f.r)`1 & (f.r)`1<=b & a<=(g.r)
  `1 & (g.r)`1<=b & c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d;
  reconsider Q=rng g as non empty Subset of TOP-REAL 2;
A7: the carrier of ((TOP-REAL 2)|Q)=[#]((TOP-REAL 2)|Q)
    .=rng g by PRE_TOPC:def 5;
  dom g=the carrier of I[01] by FUNCT_2:def 1;
  then reconsider g1=g as Function of I[01],((TOP-REAL 2)|Q) by A7,FUNCT_2:1;
  reconsider q2=g1.I as Point of TOP-REAL 2 by A5;
  reconsider q1=g1.O as Point of TOP-REAL 2 by A4;
  reconsider P=rng f as non empty Subset of TOP-REAL 2;
A8: the carrier of ((TOP-REAL 2)|P)=[#]((TOP-REAL 2)|P)
    .=rng f by PRE_TOPC:def 5;
  dom f=the carrier of I[01] by FUNCT_2:def 1;
  then reconsider f1=f as Function of I[01],((TOP-REAL 2)|P) by A8,FUNCT_2:1;
  reconsider p2=f1.I as Point of TOP-REAL 2 by A3;
  reconsider p1=f1.O as Point of TOP-REAL 2 by A2;
A9: for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1
  proof
    let p be Point of TOP-REAL 2;
    assume p in P;
    then ex x being object st x in dom f1 & p=f1.x by FUNCT_1:def 3;
    hence thesis by A2,A3,A6;
  end;
A10: for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2`2
  proof
    let p be Point of TOP-REAL 2;
    assume p in P;
    then ex x being object st x in dom f1 & p=f1.x by FUNCT_1:def 3;
    hence thesis by A4,A5,A6;
  end;
A11: for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2
  proof
    let p be Point of TOP-REAL 2;
    assume p in Q;
    then ex x being object st x in dom g1 & p=g1.x by FUNCT_1:def 3;
    hence thesis by A4,A5,A6;
  end;
A12: for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2`1
  proof
    let p be Point of TOP-REAL 2;
    assume p in Q;
    then ex x being object st x in dom g1 & p=g1.x by FUNCT_1:def 3;
    hence thesis by A2,A3,A6;
  end;
  f is Path of p1,p2 & g is Path of q1,q2 by A1,BORSUK_2:def 4;
  hence thesis by A9,A12,A10,A11,Th4;
end;

theorem
  for ar, br, cr, dr being Point of Trectangle(a,b,c,d) for h being Path
of ar,br, v being Path of dr,cr for Ar, Br, Cr, Dr being Point of TOP-REAL 2 st
Ar`1 = a & Br`1 = b & Cr`2 = c & Dr`2 = d & ar = Ar & br = Br & cr = Cr & dr =
  Dr ex s, t being Point of I[01] st h.s = v.t
proof
  let ar, br, cr, dr be Point of Trectangle(a,b,c,d);
  let h be Path of ar,br;
  let v be Path of dr,cr;
  let Ar, Br, Cr, Dr be Point of TOP-REAL 2 such that
A1: Ar`1 = a & Br`1 = b & Cr`2 = c & Dr`2 = d & ar = Ar & br = Br & cr =
  Cr & dr = Dr;
  set TR = Trectangle(a,b,c,d);
  per cases;
  suppose
A2: TR is empty;
    take 1[01], 1[01];
    thus thesis by A2;
  end;
  suppose
    TR is non empty;
    then reconsider TR = Trectangle(a,b,c,d) as non empty convex SubSpace of
    TOP-REAL 2;
    reconsider ar, br, cr, dr as Point of TR;
    reconsider h as Path of ar,br;
    reconsider v as Path of dr,cr;
A3: h.0 = ar & h.1 = br by BORSUK_2:def 4;
    the carrier of TR is Subset of TOP-REAL 2 by TSEP_1:1;
    then reconsider f = h, g = -v as Function of I[01],TOP-REAL 2 by FUNCT_2:7;
A4: (-v).0 = cr & (-v).1 = dr by BORSUK_2:def 4;
A5: for r being Point of I[01] holds a <= (f.r)`1 & (f.r)`1 <= b & a <= (g
.r)`1 & (g.r)`1 <= b & c <= (f.r)`2 & (f.r)`2 <= d & c <= (g.r)`2 & (g.r)`2 <=
    d
    proof
      let r be Point of I[01];
A6:   the carrier of TR = closed_inside_of_rectangle(a,b,c,d) by PRE_TOPC:8
        .= {p where p is Point of TOP-REAL 2: a <= p`1 & p`1 <= b & c <= p`2
      & p`2 <= d} by JGRAPH_6:def 2;
      (-v).r in the carrier of TR;
      then
A7:   ex p being Point of TOP-REAL 2 st (-v).r = p & a <= p`1 & p`1 <= b
      & c <= p`2 & p`2 <= d by A6;
      h.r in the carrier of TR;
      then
      ex p being Point of TOP-REAL 2 st h.r = p & a <= p`1 & p`1 <= b & c
      <= p`2 & p`2 <= d by A6;
      hence thesis by A7;
    end;
    f is continuous & g is continuous by PRE_TOPC:26;
    then rng f meets rng g by A1,A3,A4,A5,Th5,BORSUK_1:def 14,def 15;
    then consider y being object such that
A8: y in rng f and
A9: y in rng g by XBOOLE_0:3;
    consider t being object such that
A10: t in dom g and
A11: g.t = y by A9,FUNCT_1:def 3;
    consider s being object such that
A12: s in dom f and
A13: f.s = y by A8,FUNCT_1:def 3;
    reconsider s, t as Point of I[01] by A12,A10;
    reconsider t1 = 1-t as Point of I[01] by JORDAN5B:4;
    take s, t1;
    dr,cr are_connected by BORSUK_2:def 3;
    hence thesis by A13,A11,BORSUK_2:def 6;
  end;
end;