:: The Jordan's Property for Certain Subsets of the Plane
::  by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992-2012 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, XBOOLE_0, PRE_TOPC, REAL_1, CARD_1, XXREAL_1, XXREAL_0,
      FUNCT_1, BORSUK_1, ORDINAL2, RELAT_2, RELAT_1, SUBSET_1, FUNCOP_1,
      CONNSP_1, EUCLID, RLVECT_1, CONVEX1, RLTOPSP1, TARSKI, TOPREAL1, TOPS_2,
      STRUCT_0, ARYTM_3, MCART_1, ARYTM_1, PCOMPS_1, RCOMP_1, XREAL_0,
      ORDINAL1, METRIC_1, SQUARE_1, JORDAN1, NAT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XXREAL_0, XREAL_0, REAL_1,
      FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, NUMBERS, PRE_TOPC, TOPS_2, CONNSP_1,
      SQUARE_1, RCOMP_1, STRUCT_0, METRIC_1, PCOMPS_1, BORSUK_1, TOPREAL1,
      RLVECT_1, RLTOPSP1, EUCLID;
 constructors REAL_1, SQUARE_1, RCOMP_1, CONNSP_1, TOPS_2, TOPMETR, TOPREAL1,
      FUNCOP_1, FUNCSDOM, CONVEX1, BINOP_2, PCOMPS_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, MEMBERED, STRUCT_0,
      PRE_TOPC, BORSUK_1, EUCLID, RLTOPSP1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, CONNSP_1, XBOOLE_0, EUCLID, SQUARE_1, SUBSET_1, STRUCT_0,
      PCOMPS_1, RLTOPSP1;
 theorems TARSKI, FUNCOP_1, FUNCT_1, FUNCT_2, SUBSET_1, RCOMP_1, METRIC_1,
      PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, CONNSP_1, SQUARE_1, TOPMETR,
      TOPREAL1, EUCLID, TOPREAL3, TREAL_1, XBOOLE_0, XBOOLE_1, XREAL_0,
      XREAL_1, ZFMISC_1, SPPOL_1, XXREAL_0, RLTOPSP1;

begin

::
::  Selected theorems on connected space
::

reserve GX,GY for non empty TopSpace,
  x,y for Point of GX,
  r,s for Real;

Lm1: 0 in [.0,1.] & 1 in [.0,1.]
proof
A1: 0 in {r:0<=r & r<=1};
  1 in {s:0<=s & s<=1};
  hence thesis by A1,RCOMP_1:def 1;
end;

theorem Th1:   ::Arcwise connectedness derives connectedness
  for GX being non empty TopSpace st (for x,y being Point of GX
  ex h being Function of I[01],GX st h is continuous & x=h.0 & y=h.1)
  holds GX is connected
proof
  let GX;
  assume
A1: for x,y being Point of GX
  ex h being Function of I[01],GX st h is continuous & x=h.0 & y=h.1;
  for x,y being Point of GX ex GY st (GY is connected &
  ex f being Function of GY,GX st f is continuous & x in rng(f)& y in rng(f))
  proof
    let x,y;
    now
      consider h being Function of I[01],GX such that
A2:   h is continuous and
A3:   x=h.0 and
A4:   y=h.1 by A1;
A5:   0 in dom h by Lm1,BORSUK_1:40,FUNCT_2:def 1;
A6:   1 in dom h by Lm1,BORSUK_1:40,FUNCT_2:def 1;
A7:   x in rng h by A3,A5,FUNCT_1:def 3;
      y in rng h by A4,A6,FUNCT_1:def 3;
      hence thesis by A2,A7,TREAL_1:19;
    end;
    hence thesis;
  end;
  hence thesis by TOPS_2:63;
end;

theorem Th2:  ::Arcwise connectedness derives connectedness for subset
  for A being Subset of GX st
  (for xa,ya being Point of GX st xa in A & ya in A & xa<>ya
  ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1)
  holds A is connected
proof
  let A be Subset of GX;
  assume that
A1: for xa,ya being Point of GX st xa in A & ya in A & xa<>ya
  ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1;
  per cases;
  suppose A is non empty;
    then reconsider A as non empty Subset of GX;
A2: for xa,ya being Point of GX st xa in A & ya in A & xa = ya
    ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1
    proof
      let xa,ya be Point of GX;
      assume that
A3:   xa in A and ya in A and
A4:   xa = ya;
      reconsider xa9 = xa as Element of GX|A by A3,PRE_TOPC:8;
      reconsider h = I[01] --> xa9 as Function of I[01], GX|A;
      take h;
      thus thesis by A4,Lm1,BORSUK_1:40,FUNCOP_1:7;
    end;
    for xb,yb being Point of GX|A
    ex ha being Function of I[01],GX|A st ha is continuous & xb=ha.0 & yb=ha.1
    proof
      let xb,yb be Point of GX|A;
A5:   xb in [#](GX|A);
A6:   yb in [#](GX|A);
A7:   xb in A by A5,PRE_TOPC:def 5;
A8:   yb in A by A6,PRE_TOPC:def 5;
      per cases;
      suppose xb<>yb;
        hence thesis by A1,A7,A8;
      end;
      suppose xb = yb;
        hence thesis by A2,A7;
      end;
    end;
    then GX|A is connected by Th1;
    hence thesis by CONNSP_1:def 3;
  end;
  suppose A is empty;
    then reconsider D = A as empty Subset of GX;
    let A1, B1 be Subset of GX|A such that
    [#](GX|A) = A1 \/ B1 and A1,B1 are_separated;
    [#](GX|D) = D;
    hence thesis;
  end;
end;

theorem
  for A0 being Subset of GX, A1 being Subset of GX st
  A0 is connected & A1 is connected & A0 meets A1
  holds A0 \/ A1 is connected by CONNSP_1:1,17;

theorem Th4:
  for A0,A1,A2 being Subset of GX st
  A0 is connected & A1 is connected & A2 is connected & A0 meets A1 &
  A1 meets A2 holds A0 \/ A1 \/ A2 is connected
proof
  let A0,A1,A2 be Subset of GX;
  assume that
A1: A0 is connected and
A2: A1 is connected and
A3: A2 is connected and
A4: A0 meets A1 and
A5: A1 meets A2;
A6: A1 /\ A2 <> {} by A5,XBOOLE_0:def 7;
A7: A0 \/ A1 is connected by A1,A2,A4,CONNSP_1:1,17;
  (A0 \/ A1)/\ A2= A0 /\ A2 \/ A1 /\ A2 by XBOOLE_1:23;
  then (A0 \/ A1) meets A2 by A6,XBOOLE_0:def 7;
  hence thesis by A3,A7,CONNSP_1:1,17;
end;

theorem Th5:
  for A0,A1,A2,A3 being Subset of GX st A0 is connected & A1 is connected &
  A2 is connected & A3 is connected & A0 meets A1 & A1 meets A2 &
  A2 meets A3 holds A0 \/ A1 \/ A2 \/ A3 is connected
proof
  let A0,A1,A2,A3 be Subset of GX;
  assume that
A1: A0 is connected and
A2: A1 is connected and
A3: A2 is connected and
A4: A3 is connected and
A5: A0 meets A1 and
A6: A1 meets A2 and
A7: A2 meets A3;
A8: A2 /\ A3 <> {} by A7,XBOOLE_0:def 7;
A9: A0 \/ A1 \/ A2 is connected by A1,A2,A3,A5,A6,Th4;
  (A0 \/ A1 \/ A2)/\ A3= (A0 \/ A1) /\ A3 \/ A2 /\ A3 by XBOOLE_1:23;
  then (A0 \/ A1 \/ A2) meets A3 by A8,XBOOLE_0:def 7;
  hence thesis by A4,A9,CONNSP_1:1,17;
end;

begin

::
:: Certain connected and open subsets in the Euclidean plane
::

reserve Q,P1,P2 for Subset of TOP-REAL 2;
reserve P for Subset of TOP-REAL 2;
reserve w1,w2 for Point of TOP-REAL 2;

definition
  let V be RealLinearSpace, P be Subset of V;
  redefine attr P is convex means
  for w1,w2 being Element of V st w1 in P & w2 in P holds LSeg(w1,w2) c= P;
  compatibility by RLTOPSP1:22;
end;

registration let n be Nat;
 cluster convex -> connected for Subset of TOP-REAL n;
 coherence
proof
  let P be Subset of TOP-REAL n;
  assume that
A1: for w3,w4 being Point of TOP-REAL n st w3 in P & w4 in P holds
  LSeg(w3,w4) c= P;
  for w1,w2 being Point of TOP-REAL n st w1 in P & w2 in P & w1<>w2
  ex h being Function of I[01],(TOP-REAL n)|P st h is continuous
  & w1=h.0 & w2=h.1
  proof
    let w1,w2 be Point of TOP-REAL n;
    assume that
A2: w1 in P and
A3: w2 in P and
A4: w1<>w2;
A5: LSeg(w1,w2) c= P by A1,A2,A3;
    LSeg(w1,w2) is_an_arc_of w1,w2 by A4,TOPREAL1:9;
    then consider f being Function of I[01], (TOP-REAL n)|LSeg(w1,w2) such that
A6: f is being_homeomorphism and
A7: f.0 = w1 and
A8: f.1 = w2 by TOPREAL1:def 1;
A9: f is continuous by A6,TOPS_2:def 5;
A10: rng f = [#]((TOP-REAL n)|LSeg(w1,w2)) by A6,TOPS_2:def 5;
    then
A11: rng f c= P by A5,PRE_TOPC:def 5;
    then [#]((TOP-REAL n)|LSeg(w1,w2)) c= [#]((TOP-REAL n)|P)
    by A10,PRE_TOPC:def 5;
    then
A12: (TOP-REAL n)|LSeg(w1,w2) is SubSpace of (TOP-REAL n)|P by TOPMETR:3;
    dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
    then reconsider g=f as Function of [.0,1.],P by A11,FUNCT_2:2;
    the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P)
      .= P by PRE_TOPC:def 5;
    then reconsider gt=g as Function of I[01],(TOP-REAL n)|P by BORSUK_1:40;
    gt is continuous by A9,A12,PRE_TOPC:26;
    hence thesis by A7,A8;
  end;
  hence thesis by Th2;
end;
end;

reserve pa,pb for Point of TOP-REAL 2,
  s1,t1,s2,t2,s,t,s3,t3,s4,t4,s5,t5,s6,t6, l,sa,sd,ta,td for Real;
reserve s1a,t1a,s2a,t2a,s3a,t3a,sb,tb,sc,tc for Real;

Lm2: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;

Lm3: for s1 holds { |[ sb,tb ]|:sb<s1} is Subset of REAL 2
proof
  let s1;
  { |[ sb,tb ]|:sb<s1} c= REAL 2
  proof
    let y be set;
    assume y in { |[ sb,tb ]|:sb<s1};
    then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and s7<s1;
    |[ s7,t7 ]| in the carrier of TOP-REAL 2;
    hence thesis by A1,EUCLID:22;
  end;
  hence thesis;
end;

Lm4: for t1 holds { |[ sb,tb ]| :tb<t1} is Subset of REAL 2
proof
  let t1;
  { |[ sd,td ]|:td<t1} c= REAL 2
  proof
    let y be set;
    assume y in { |[ sd,td ]|:td<t1};
    then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and t7<t1;
    |[ s7,t7 ]| in the carrier of TOP-REAL 2;
    hence thesis by A1,EUCLID:22;
  end;
  hence thesis;
end;

Lm5: for s2 holds { |[ sb,tb ]| :s2<sb} is Subset of REAL 2
proof
  let s2;
  { |[ sb,tb ]|:s2<sb} c= REAL 2
  proof
    let y be set;
    assume y in { |[ sb,tb ]|:s2<sb};
    then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and s2<s7;
    |[ s7,t7 ]| in the carrier of TOP-REAL 2;
    hence thesis by A1,EUCLID:22;
  end;
  hence thesis;
end;

Lm6: for t2 holds { |[ sb,tb ]|:t2<tb} is Subset of REAL 2
proof
  let t2;
  { |[ sb,tb ]|:t2<tb} c= REAL 2
  proof
    let y be set;
    assume y in { |[ sb,tb ]|:t2<tb};
    then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and t2<t7;
    |[ s7,t7 ]| in the carrier of TOP-REAL 2;
    hence thesis by A1,EUCLID:22;
  end;
  hence thesis;
end;

Lm7: for s1,s2,t1,t2 holds { |[ s,t ]| where s is Real,t is Real:
s1<s & s<s2 & t1<t & t<t2} is Subset of REAL 2
proof
  let s1,s2,t1,t2;
  { |[ sb,tb ]| where sb is Real, tb is Real:
  s1<sb & sb<s2 & t1<tb & tb<t2} c= REAL 2
  proof
    let y be set;
    assume y in { |[ sb,tb ]| where sb is Real,tb is Real:
    s1<sb & sb<s2 & t1<tb & tb<t2};
    then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and s1<s7
    and s7<s2
    and t1<t7
    and t7<t2;
    |[ s7,t7 ]| in the carrier of TOP-REAL 2;
    hence thesis by A1,EUCLID:22;
  end;
  hence thesis;
end;

Lm8: for s1,s2,t1,t2 holds
{ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} is Subset of REAL 2
proof
  let s1,s2,t1,t2;
  { |[ sb,tb ]| where sb is Real,tb is Real:
  not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} c= REAL 2
  proof
    let y be set;
    assume y in { |[ sb,tb ]| where sb is Real,tb is Real:
    not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
    then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and not (s1<=s7 & s7<=s2 & t1<=t7 & t7<=t2);
    |[ s7,t7 ]| in the carrier of TOP-REAL 2;
    hence thesis by A1,EUCLID:22;
  end;
  hence thesis;
end;

canceled;

theorem Th7:
  {|[ s,t ]|: s1<s & s<s2 & t1<t & t<t2} =
  {|[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2} /\ {|[s5,t5]|:t1<t5} /\
  {|[s6,t6]|:t6<t2}
proof
  now
    let x be set;
    assume x in { |[ s,t ]|: s1<s & s<s2 & t1<t & t<t2};
    then
A1: ex s,t st |[s,t]|=x & s1<s & s<s2 & t1<t & t<t2;
    then
A2: x in { |[ s3,t3 ]|:s1<s3};
    x in { |[ s4,t4 ]|:s4<s2} by A1;
    then
A3: x in { |[ s3,t3 ]|:s1<s3} /\ { |[ s4,t4 ]|:s4<s2} by A2,XBOOLE_0:def 4;
A4: x in { |[ s5,t5 ]|:t1<t5} by A1;
A5: x in { |[ s6,t6 ]|:t6<t2} by A1;
    x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5} by A3,A4
,XBOOLE_0:def 4;
    hence
    x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
    /\ {|[s6,t6]|:t6<t2} by A5,XBOOLE_0:def 4;
  end;
  then
A6: { |[ s,t ]|: s1<s & s<s2 & t1<t & t<t2} c=
  { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
  /\ {|[s6,t6]|:t6<t2} by TARSKI:def 3;
  now
    let x be set;
    assume
    A7: x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5 }
    /\ {|[s6,t6]|:t6<t2};
    then
A8: x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5} by
XBOOLE_0:def 4;
    then
A9: x in { |[ s3,t3 ]|:s1<s3} /\ { |[ s4,t4]|:s4<s2} by XBOOLE_0:def 4;
A10: x in { |[ s6,t6 ]|:t6<t2} by A7,XBOOLE_0:def 4;
A11: x in { |[ s3,t3 ]|:s1<s3} by A9,XBOOLE_0:def 4;
A12: x in { |[ s4,t4 ]|:s4<s2} by A9,XBOOLE_0:def 4;
A13: x in { |[ s5,t5 ]|:t1<t5} by A8,XBOOLE_0:def 4;
A14: ex sa,ta st |[sa,ta]|=x & s1<sa by A11;
A15: ex sb,tb st |[sb,tb]|=x & sb< s2 by A12;
A16: ex sc,tc st |[sc,tc]|=x & t1<tc by A13;
A17: ex sd,td st |[sd,td]|=x & td<t2 by A10;
    consider sa,ta such that
A18: |[sa,ta]|=x and
A19: s1<sa by A11;
    reconsider p=x as Point of TOP-REAL 2 by A14;
A20: p`1=sa by A18,EUCLID:52;
A21: p`2=ta by A18,EUCLID:52;
A22: sa<s2 by A15,A20,EUCLID:52;
A23: t1<ta by A16,A21,EUCLID:52;
    ta<t2 by A17,A21,EUCLID:52;
    hence x in { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2} by A18,A19,A22,A23;
  end;
  then { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
  /\ {|[s6,t6]|:t6<t2}c={ |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
  by TARSKI:def 3;
  hence thesis by A6,XBOOLE_0:def 10;
end;

theorem Th8:
  {|[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} =
  {|[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1} \/ {|[s5,t5]|:s2<s5} \/
  {|[s6,t6]|:t2<t6}
proof
  now
    let x be set;
    assume x in { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
    then ex s,t st |[s,t]|=x & not (s1<=s & s<=s2 & t1<=t & t<=t2);
    then x in { |[ s3,t3 ]|:s3<s1}or x in { |[ s4,t4 ]|:t4<t1}
    or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6};
    then x in { |[ s3,t3 ]|:s3<s1} \/ { |[ s4,t4 ]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3;
    then x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
    or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3;
    hence
    x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
    \/ {|[s6,t6]|:t2<t6} by XBOOLE_0:def 3;
  end;
  then
A1: { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} c=
  { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
  \/ {|[s6,t6]|:t2<t6} by TARSKI:def 3;
  now
    let x be set;
    assume x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2< s5
    } \/ {|[s6,t6]|:t2<t6};
    then x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
    or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3;
    then x in { |[ s3,t3 ]|:s3<s1} \/ { |[ s4,t4]|:t4<t1}
    or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3
    ;
    then x in { |[ s3,t3 ]|:s3<s1} or x in { |[ s4,t4 ]|:t4<t1}
    or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3
    ;
    then (ex sa,ta st |[sa,ta]|=x & sa<s1)
    or (ex sc,tc st |[sc,tc]|=x & tc<t1) or (ex sb,tb st |[sb,tb]|=x & s2<sb)
    or ex sd,td st |[sd,td]|=x & t2<td;
    hence x in { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
  end;
  then { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
  \/ {|[s6,t6]|:t2<t6}c={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)}
  by TARSKI:def 3;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th9:
  for s1,t1,s2,t2,P st P = {|[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
  holds P is convex
proof
  let s1,t1,s2,t2,P;
  assume
A1: P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
  let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
  let x be set such that
A4: x in LSeg(w1,w2);
  consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: s1<s3 and
A7: s3<s2 and
A8: t1<t3 and
A9: t3<t2 by A1,A2;
A10: w1`1=s3 by A5,EUCLID:52;
A11: w1`2=t3 by A5,EUCLID:52;
  consider s4,t4 such that
A12: |[ s4,t4 ]|=w2 and
A13: s1<s4 and
A14: s4<s2 and
A15: t1<t4 and
A16: t4<t2 by A1,A3;
A17: w2`1=s4 by A12,EUCLID:52;
A18: w2`2=t4 by A12,EUCLID:52;
  consider l such that
A19: x = (1-l)*w1 + l*w2 and
A20: 0 <= l and
A21: l <= 1 by A4;
  set w = (1-l)*w1 + l*w2;
A22: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A23: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A24: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A25: ((1-l)*w1)`1= (1-l)*w1`1 by A23,EUCLID:52;
A26: ((1-l)*w1)`2= (1-l)*w1`2 by A23,EUCLID:52;
A27: (l*w2)`1=l*w2`1 by A24,EUCLID:52;
A28: (l*w2)`2=l*w2`2 by A24,EUCLID:52;
A29: w`1=(1-l)* w1`1+ l* w2`1 by A22,A25,A27,EUCLID:52;
A30: w`2=(1-l)* w1`2+ l* w2`2 by A22,A26,A28,EUCLID:52;
A31: s1< w`1 by A6,A10,A13,A17,A20,A21,A29,XREAL_1:175;
A32: w`1<s2 by A7,A10,A14,A17,A20,A21,A29,XREAL_1:176;
A33: t1< w`2 by A8,A11,A15,A18,A20,A21,A30,XREAL_1:175;
A34: w`2<t2 by A9,A11,A16,A18,A20,A21,A30,XREAL_1:176;
  w = |[w`1, w`2]| by EUCLID:53;
  hence thesis by A1,A19,A31,A32,A33,A34;
end;

canceled;

theorem Th11:
  for s1,P st P = { |[ s,t ]|:s1<s } holds P is convex
proof
  let s1,P;
  assume
A1: P = { |[ s,t ]|:s1<s };
  let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
  let x be set such that
A4: x in LSeg(w1,w2);
  consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: s1<s3 by A1,A2;
A7: w1`1=s3 by A5,EUCLID:52;
  consider s4,t4 such that
A8: |[ s4,t4 ]|=w2 and
A9: s1<s4 by A1,A3;
A10: w2`1=s4 by A8,EUCLID:52;
  consider l such that
A11: x = (1-l)*w1 + l*w2 and
A12: 0 <= l and
A13: l <= 1 by A4;
  set w = (1-l)*w1 + l*w2;
A14: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A15: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A16: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A17: ((1-l)*w1)`1= (1-l)*w1`1 by A15,EUCLID:52;
  (l*w2)`1=l*w2`1 by A16,EUCLID:52;
  then w`1=(1-l)* w1`1+ l* w2`1 by A14,A17,EUCLID:52;
  then
A18: s1< w`1 by A6,A7,A9,A10,A12,A13,XREAL_1:175;
  w = |[w`1, w`2]| by EUCLID:53;
  hence thesis by A1,A11,A18;
end;

canceled;

theorem Th13:
  for s2,P st P = {|[ s,t ]|:s<s2 } holds P is convex
proof
  let s2,P;
  assume
A1: P = { |[ s,t ]|:s<s2 };
  let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
  let x be set such that
A4: x in LSeg(w1,w2);
  consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: s3<s2 by A1,A2;
A7: w1`1=s3 by A5,EUCLID:52;
  consider s4,t4 such that
A8: |[ s4,t4 ]|=w2 and
A9: s4<s2 by A1,A3;
A10: w2`1=s4 by A8,EUCLID:52;
  consider l such that
A11: x = (1-l)*w1 + l*w2 and
A12: 0 <= l and
A13: l <= 1 by A4;
  set w = (1-l)*w1 + l*w2;
A14: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A15: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A16: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A17: ((1-l)*w1)`1= (1-l)*w1`1 by A15,EUCLID:52;
  (l*w2)`1=l*w2`1 by A16,EUCLID:52;
  then w`1=(1-l)* w1`1+ l* w2`1 by A14,A17,EUCLID:52;
  then
A18: s2> w`1 by A6,A7,A9,A10,A12,A13,XREAL_1:176;
  w = |[w`1, w`2]| by EUCLID:53;
  hence thesis by A1,A11,A18;
end;

canceled;

theorem Th15:
  for t1,P st P = {|[ s,t ]|:t1<t } holds P is convex
proof
  let t1,P;
  assume
A1: P = { |[ s,t ]|:t1<t };
  let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
  let x be set such that
A4: x in LSeg(w1,w2);
  consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: t1<t3 by A1,A2;
A7: w1`2=t3 by A5,EUCLID:52;
  consider s4,t4 such that
A8: |[ s4,t4 ]|=w2 and
A9: t1<t4 by A1,A3;
A10: w2`2=t4 by A8,EUCLID:52;
  consider l such that
A11: x = (1-l)*w1 + l*w2 and
A12: 0 <= l and
A13: l <= 1 by A4;
  set w = (1-l)*w1 + l*w2;
A14: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A15: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A16: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A17: ((1-l)*w1)`2= (1-l)*w1`2 by A15,EUCLID:52;
  (l*w2)`2=l*w2`2 by A16,EUCLID:52;
  then w`2=(1-l)* w1`2+ l* w2`2 by A14,A17,EUCLID:52;
  then
A18: t1< w`2 by A6,A7,A9,A10,A12,A13,XREAL_1:175;
  w = |[w`1, w`2]| by EUCLID:53;
  hence thesis by A1,A11,A18;
end;

canceled;

theorem Th17:
  for t2,P st P = { |[ s,t ]|: t<t2 } holds P is convex
proof
  let t2,P;
  assume
A1: P = { |[ s,t ]|:t<t2 };
  let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
  let x be set such that
A4: x in LSeg(w1,w2);
  consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: t3<t2 by A1,A2;
A7: w1`2=t3 by A5,EUCLID:52;
  consider s4,t4 such that
A8: |[ s4,t4 ]|=w2 and
A9: t4<t2 by A1,A3;
A10: w2`2=t4 by A8,EUCLID:52;
  consider l such that
A11: x = (1-l)*w1 + l*w2 and
A12: 0 <= l and
A13: l <= 1 by A4;
  set w = (1-l)*w1 + l*w2;
A14: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A15: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A16: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A17: ((1-l)*w1)`2= (1-l)*w1`2 by A15,EUCLID:52;
  (l*w2)`2=l*w2`2 by A16,EUCLID:52;
  then w`2=(1-l)* w1`2+ l* w2`2 by A14,A17,EUCLID:52;
  then
A18: t2> w`2 by A6,A7,A9,A10,A12,A13,XREAL_1:176;
  w = |[w`1, w`2]| by EUCLID:53;
  hence thesis by A1,A11,A18;
end;

canceled;

theorem Th19:
  for s1,t1,s2,t2,P st P = { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)}
  holds P is connected
proof
  let s1,t1,s2,t2,P;
  assume P={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
  then
A1: P={ |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
  \/ {|[s6,t6]|:t2<t6} by Th8;
  reconsider A0={ |[ s,t ]|:s<s1}, A1={ |[ s,t ]|:t<t1},
  A2={ |[ s,t ]|:s2<s}, A3={ |[ s,t ]|:t2<t}
  as Subset of TOP-REAL 2 by Lm2,Lm3,Lm4,Lm5,Lm6;
A2: s1-1<s1 by XREAL_1:44;
A3: t1-1<t1 by XREAL_1:44;
A4: |[s1-1,t1-1]| in A0 by A2;
  |[s1-1,t1-1]| in A1 by A3;
  then A0 /\ A1 <> {} by A4,XBOOLE_0:def 4;
  then
A5: A0 meets A1 by XBOOLE_0:def 7;
A6: s2< s2+1 by XREAL_1:29;
A7: |[s2+1,t1-1]| in A1 by A3;
  |[s2+1,t1-1]| in A2 by A6;
  then A1 /\ A2 <> {} by A7,XBOOLE_0:def 4;
  then
A8: A1 meets A2 by XBOOLE_0:def 7;
A9: t2< t2+1 by XREAL_1:29;
A10: |[s2+1,t2+1]| in A2 by A6;
  |[s2+1,t2+1]| in A3 by A9;
  then A2 /\ A3 <> {} by A10,XBOOLE_0:def 4;
  then
A11: A2 meets A3 by XBOOLE_0:def 7;
A12: A0 is convex by Th13;
A13: A1 is convex by Th17;
A14: A2 is convex by Th11;
  A3 is convex by Th15;
  hence thesis by A1,A5,A8,A11,A12,A13,A14,Th5;
end;

Lm9: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;

theorem Th20:
  for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1<s } holds
  P is open
proof
  let s1;
  let P be Subset of TOP-REAL 2 such that
A1: P= { |[ s,t ]|:s1<s };
  reconsider PP=P as Subset of TopSpaceMetr Euclid 2 by Lm9;
  for pe being Point of Euclid 2 st pe in P ex r being real number st r>0 &
  Ball(pe,r) c= P
  proof
    let pe be Point of Euclid 2;
    assume pe in P;
    then consider s,t such that
A2: |[ s,t ]|=pe and
A3: s1<s by A1;
    set r=(s-s1)/2;
A4: s-s1>0 by A3,XREAL_1:50;
    then
A5: r>0 by XREAL_1:139;
    Ball(pe,r) c= P
    proof
      let x be set;
      assume x in Ball(pe,r);
      then x in {q where q is Element of Euclid 2:dist(pe,q)<r} by METRIC_1:17;
      then consider q being Element of Euclid 2 such that
A6:   q=x and
A7:   dist(pe,q)<r;
      reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by EUCLID:22;
      (Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
      then
A8:   sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A7,TOPREAL3:7;
A9:   0 <= (ppe`1 - pq`1)^2 by XREAL_1:63;
      0 <= (ppe`2 - pq`2)^2 by XREAL_1:63;
      then
A10:  0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A9,XREAL_1:7;
      then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 2;
      then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
      by A8,SQUARE_1:16;
      then
A11:  (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A10,SQUARE_1:def 2;
      (ppe`1 - pq`1)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by XREAL_1:31,63;
      then (ppe`1 - pq`1)^2 <r^2 by A11,XXREAL_0:2;
      then ppe`1 - pq`1 < r by A5,SQUARE_1:15;
      then ppe`1 <pq`1+r by XREAL_1:19;
      then ppe`1 - r < pq`1 by XREAL_1:19;
      then
A12:  s-(s-s1)/2 < pq`1 by A2,EUCLID:52;
      s-(s-s1)/2 =r+s1;
      then
A13:  s1< s-(s-s1)/2 by A4,XREAL_1:29,139;
A14:  |[pq`1,pq`2]|=x by A6,EUCLID:53;
      s1<pq`1 by A12,A13,XXREAL_0:2;
      hence thesis by A1,A14;
    end;
    hence thesis by A4,XREAL_1:139;
  end;
  then PP is open by TOPMETR:15;
  hence thesis by Lm9,PRE_TOPC:30;
end;

theorem Th21:
  for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1>s } holds
  P is open
proof
  let s1;
  let P be Subset of TOP-REAL 2 such that
A1: P= { |[ s,t ]|:s1>s };
  reconsider PP=P as Subset of TopSpaceMetr Euclid 2 by Lm9;
  for pe being Point of Euclid 2 st pe in P ex r being real number st
  r>0 & Ball(pe,r) c= P
  proof
    let pe be Point of Euclid 2;
    assume pe in P;
    then consider s,t such that
A2: |[ s,t ]|=pe and
A3: s1>s by A1;
    set r=(s1-s)/2;
A4: s1-s>0 by A3,XREAL_1:50;
    then
A5: r>0 by XREAL_1:139;
    Ball(pe,r) c= P
    proof
      let x be set;
      assume x in Ball(pe,r);
      then x in {q where q is Element of Euclid 2:dist(pe,q)<r} by METRIC_1:17;
      then consider q being Element of Euclid 2 such that
A6:   q=x and
A7:   dist(pe,q)<r;
      reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by EUCLID:22;
      (Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
      then
A8:   sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A7,TOPREAL3:7;
A9:   0 <= (ppe`1 - pq`1)^2 by XREAL_1:63;
      0 <= (ppe`2 - pq`2)^2 by XREAL_1:63;
      then
A10:  0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A9,XREAL_1:7;
      then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 2;
      then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
      by A8,SQUARE_1:16;
      then
A11:  (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A10,SQUARE_1:def 2;
      (ppe`1 - pq`1)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by XREAL_1:31,63;
      then (pq`1-ppe`1)^2 <r^2 by A11,XXREAL_0:2;
      then pq`1-ppe`1 < r by A5,SQUARE_1:15;
      then ppe`1 + r > pq`1 by XREAL_1:19;
      then
A12:  s+(s1-s)/2 > pq`1 by A2,EUCLID:52;
      s+(s1-s)/2 =s1-r;
      then
A13:  s1> s+(s1-s)/2 by A4,XREAL_1:44,139;
A14:  |[pq`1,pq`2]|=x by A6,EUCLID:53;
      s1>pq`1 by A12,A13,XXREAL_0:2;
      hence thesis by A1,A14;
    end;
    hence thesis by A4,XREAL_1:139;
  end;
  then PP is open by TOPMETR:15;
  hence thesis by Lm9,PRE_TOPC:30;
end;

theorem Th22:
  for s1 for P being Subset of TOP-REAL 2 st
  P = { |[ s,t ]|:s1<t } holds P is open
proof
  let s1;
  let P be Subset of TOP-REAL 2 such that
A1: P= { |[ s,t ]|:s1<t };
  reconsider PP=P as Subset of TopSpaceMetr Euclid 2 by Lm9;
  for pe being Point of Euclid 2 st pe in P ex r being real number
  st r>0 & Ball(pe,r) c= P
  proof
    let pe be Point of Euclid 2;
    assume pe in P;
    then consider s,t such that
A2: |[ s,t ]|=pe and
A3: s1<t by A1;
    set r=(t-s1)/2;
A4: t-s1>0 by A3,XREAL_1:50;
    then
A5: r>0 by XREAL_1:139;
    Ball(pe,r) c= P
    proof
      let x be set;
      assume x in Ball(pe,r);
      then x in {q where q is Element of Euclid 2:dist(pe,q)<r} by METRIC_1:17;
      then consider q being Element of Euclid 2 such that
A6:   q=x and
A7:   dist(pe,q)<r;
      reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by EUCLID:22;
      (Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
      then
A8:   sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A7,TOPREAL3:7;
A9:   0 <= (ppe`1 - pq`1)^2 by XREAL_1:63;
      0 <= (ppe`2 - pq`2)^2 by XREAL_1:63;
      then
A10:  0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A9,XREAL_1:7;
      then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 2;
      then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
      by A8,SQUARE_1:16;
      then
A11:  (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A10,SQUARE_1:def 2;
      (ppe`2 - pq`2)^2 <= (ppe`2 - pq`2)^2+(ppe`1 - pq`1)^2 by XREAL_1:31,63;
      then (ppe`2 - pq`2)^2 <r^2 by A11,XXREAL_0:2;
      then ppe`2 - pq`2 < r by A5,SQUARE_1:15;
      then ppe`2 <pq`2+r by XREAL_1:19;
      then ppe`2 - r < pq`2 by XREAL_1:19;
      then
A12:  t-(t-s1)/2 < pq`2 by A2,EUCLID:52;
      t-(t-s1)/2 =r+s1;
      then
A13:  s1< t-(t-s1)/2 by A4,XREAL_1:29,139;
A14:  |[pq`1,pq`2]|=x by A6,EUCLID:53;
      s1<pq`2 by A12,A13,XXREAL_0:2;
      hence thesis by A1,A14;
    end;
    hence thesis by A4,XREAL_1:139;
  end;
  then PP is open by TOPMETR:15;
  hence thesis by Lm9,PRE_TOPC:30;
end;

theorem Th23:
  for s1 for P being Subset of TOP-REAL 2 st P = { |[ s,t ]|:s1>t } holds
  P is open
proof
  let s1;
  let P be Subset of TOP-REAL 2 such that
A1: P= { |[ s,t ]|:s1>t };
  reconsider PP=P as Subset of TopSpaceMetr Euclid 2 by Lm9;
  for pe being Point of Euclid 2 st pe in P ex r being real number st r>0 &
  Ball(pe,r) c= P
  proof
    let pe be Point of Euclid 2;
    assume pe in P;
    then consider s,t such that
A2: |[ s,t ]|=pe and
A3: s1>t by A1;
    set r=(s1-t)/2;
A4: s1-t>0 by A3,XREAL_1:50;
    then
A5: r>0 by XREAL_1:139;
    Ball(pe,r) c= P
    proof
      let x be set;
      assume x in Ball(pe,r);
      then x in {q where q is Element of Euclid 2:dist(pe,q)<r} by METRIC_1:17;
      then consider q being Element of Euclid 2 such that
A6:   q=x and
A7:   dist(pe,q)<r;
      reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by EUCLID:22;
      (Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
      then
A8:   sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A7,TOPREAL3:7;
A9:   0 <= (ppe`1 - pq`1)^2 by XREAL_1:63;
      0 <= (ppe`2 - pq`2)^2 by XREAL_1:63;
      then
A10:  0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A9,XREAL_1:7;
      then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 2;
      then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
      by A8,SQUARE_1:16;
      then
A11:  (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A10,SQUARE_1:def 2;
      (ppe`2 - pq`2)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by XREAL_1:31,63;
      then (pq`2-ppe`2)^2 <r^2 by A11,XXREAL_0:2;
      then pq`2-ppe`2 < r by A5,SQUARE_1:15;
      then ppe`2 + r > pq`2 by XREAL_1:19;
      then
A12:  t+(s1-t)/2 > pq`2 by A2,EUCLID:52;
      t+(s1-t)/2 =s1-r;
      then
A13:  s1> t+(s1-t)/2 by A4,XREAL_1:44,139;
A14:  |[pq`1,pq`2]|=x by A6,EUCLID:53;
      s1>pq`2 by A12,A13,XXREAL_0:2;
      hence thesis by A1,A14;
    end;
    hence thesis by A4,XREAL_1:139;
  end;
  then PP is open by TOPMETR:15;
  hence thesis by Lm9,PRE_TOPC:30;
end;

theorem Th24:
  for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
  P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2} holds P is open
proof
  let s1,t1,s2,t2;
  let P be Subset of TOP-REAL 2;
  assume
A1: P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
  reconsider P1={|[s,t]|:s1<s} as Subset of TOP-REAL 2 by Lm2,Lm5;
  reconsider P2={|[s,t]|:s<s2} as Subset of TOP-REAL 2 by Lm2,Lm3;
  reconsider P3={|[s,t]|:t1<t} as Subset of TOP-REAL 2 by Lm2,Lm6;
  reconsider P4={|[s,t]|:t<t2} as Subset of TOP-REAL 2 by Lm2,Lm4;
A2: P=P1 /\ P2 /\ P3 /\ P4 by A1,Th7;
A3: P1 is open by Th20;
  P2 is open by Th21;
  then
A4: P1 /\ P2 is open by A3,TOPS_1:11;
A5: P3 is open by Th22;
A6: P4 is open by Th23;
  P1 /\ P2 /\ P3 is open by A4,A5,TOPS_1:11;
  hence thesis by A2,A6,TOPS_1:11;
end;

theorem Th25:
  for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
  P = { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} holds P is open
proof
  let s1,t1,s2,t2;
  let P be Subset of TOP-REAL 2;
  assume P={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
  then
A1: P={ |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
  \/ {|[s6,t6]|:t2<t6} by Th8;
  reconsider A0={ |[ s,t ]|:s<s1} as Subset of TOP-REAL 2 by Lm2,Lm3;
  reconsider A1={ |[ s,t ]|:t<t1} as Subset of TOP-REAL 2 by Lm2,Lm4;
  reconsider A2={ |[ s,t ]|:s2<s} as Subset of TOP-REAL 2 by Lm2,Lm5;
  reconsider A3={ |[ s,t ]|:t2<t} as Subset of TOP-REAL 2 by Lm2,Lm6;
A2: A0 is open by Th21;
  A1 is open by Th23;
  then
A3: A0 \/ A1 is open by A2,TOPS_1:10;
  A2 is open by Th20;
  then
A4: A0 \/ A1 \/ A2 is open by A3,TOPS_1:10;
  A3 is open by Th22;
  hence thesis by A1,A4,TOPS_1:10;
end;

theorem Th26:
  for s1,t1,s2,t2,P,Q st P = { |[ sa,ta ]|:s1<sa & sa<s2 & t1<ta & ta<t2} &
  Q = { |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} holds P misses Q
proof
  let s1,t1,s2,t2,P,Q;
  assume that
A1: P = { |[ sa,ta ]|:s1<sa & sa<s2 & t1<ta & ta<t2} and
A2: Q = { |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
  assume not thesis;
  then consider x be set such that
A3: x in P and
A4: x in Q by XBOOLE_0:3;
  consider sa,ta such that
A5: |[sa,ta]|=x and
A6: s1<sa and
A7: sa<s2 and
A8: t1<ta and
A9: ta<t2 by A1,A3;
A10: ex sb,tb st ( |[sb,tb]|=x)&( not (s1<=sb & sb<=s2 & t1<=tb
  & tb<=t2)) by A2,A4;
  set p= |[sa,ta]|;
A11: p`1=sa by EUCLID:52;
  p`2=ta by EUCLID:52;
  hence contradiction by A5,A6,A7,A8,A9,A10,A11,EUCLID:52;
end;

theorem Th27:
  for s1,s2,t1,t2 be Real holds
  {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} =
  {|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2}
proof
  let s1,s2,t1,t2;
  now
    let x be set;
A1: now
      assume x in
      {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2};
      then consider pp being Point of TOP-REAL 2 such that
A2:   pp=x and
A3:   s1<pp`1 and
A4:   pp`1<s2 and
A5:   t1<pp`2 and
A6:   pp`2<t2;
      |[pp`1,pp`2]|=x by A2,EUCLID:53;
      hence
      x in {|[s1a,t1a]|:s1<s1a & s1a<s2 & t1<t1a & t1a<t2} by A3,A4,A5,A6;
    end;
    now
      assume x in {|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2};
      then consider sa,ta being Real such that
A7:   |[sa,ta]|=x and
A8:   s1<sa and
A9:   sa<s2 and
A10:  t1<ta and
A11:  ta<t2;
      set pa=|[sa,ta]|;
A12:  s1<pa`1 by A8,EUCLID:52;
A13:  pa`1<s2 by A9,EUCLID:52;
A14:  t1<pa`2 by A10,EUCLID:52;
      pa`2<t2 by A11,EUCLID:52;
      hence x in
      {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2}
      by A7,A12,A13,A14;
    end;
    hence x in
    {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2}
    iff x in {|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by A1;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th28:
  for s1,s2,t1,t2 holds {qc where qc is Point of TOP-REAL 2:
  not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} =
  {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)}
proof
  let s1,s2,t1,t2;
  now
    let x be set;
A1: now
      assume x in {qc where qc is Point of TOP-REAL 2:
      not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)};
      then consider q being Point of TOP-REAL 2 such that
A2:   q=x and
A3:   not (s1<=q`1 & q`1<=s2 & t1<=q`2 & q`2<=t2);
      |[q`1,q`2]|=x by A2,EUCLID:53;
      hence
      x in {|[s2a,t2a]| : not (s1<=s2a & s2a<=s2 & t1<=t2a & t2a<=t2)} by A3;
    end;
    now
      assume x in {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
      then consider sb,tb being Real such that
A4:   |[sb,tb]|=x and
A5:   not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2);
      set qa=|[sb,tb]|;
      not (s1<=qa`1 & qa`1<=s2 & t1<=qa`2 & qa`2<=t2) by A5,EUCLID:52;
      hence x in {qc where qc is Point of TOP-REAL 2:
      not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} by A4;
    end;
    hence x in {qc where qc is Point of TOP-REAL 2:
    not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} iff x in {|[sb,tb]| :
    not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by A1;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th29:
  for s1,s2,t1,t2 holds
  { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2 & t1<p0`2 & p0`2<t2}
  is Subset of TOP-REAL 2
proof
  let s1,s2,t1,t2;
  { |[ sc,tc ]|: s1<sc & sc<s2 & t1<tc & tc<t2}
  is Subset of TOP-REAL 2 by Lm2,Lm7;
  hence thesis by Th27;
end;

theorem Th30:
  for s1,s2,t1,t2 holds { pq where pq is Point of TOP-REAL 2:
  not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} is Subset of TOP-REAL 2
proof
  let s1,s2,t1,t2;
  { |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)}
  is Subset of TOP-REAL 2 by Lm2,Lm8;
  hence thesis by Th28;
end;

theorem Th31:
  for s1,t1,s2,t2,P st
  P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
  & t1<p0`2 & p0`2<t2} holds P is convex
proof
  let s1,t1,s2,t2,P;
  assume P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
  & t1<p0`2 & p0`2<t2};
  then P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by Th27;
  hence thesis by Th9;
end;

theorem Th32:
  for s1,t1,s2,t2,P st P = { pq where pq is Point of TOP-REAL 2:
  not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} holds P is connected
proof
  let s1,t1,s2,t2,P;
  assume P= { pq where pq is Point of TOP-REAL 2:
  not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)};
  then P = {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by Th28;
  hence thesis by Th19;
end;

theorem Th33:
  for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
  P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
  & t1<p0`2 & p0`2<t2} holds P is open
proof
  let s1,t1,s2,t2;
  let P be Subset of TOP-REAL 2;
  assume P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
  & t1<p0`2 & p0`2<t2};
  then P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by Th27;
  hence thesis by Th24;
end;

theorem Th34:
  for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
  P = { pq where pq is Point of TOP-REAL 2:
  not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} holds P is open
proof
  let s1,t1,s2,t2;
  let P be Subset of TOP-REAL 2;
  assume P= { pq where pq is Point of TOP-REAL 2:
  not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)};
  then P = {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by Th28;
  hence thesis by Th25;
end;

theorem Th35:
  for s1,t1,s2,t2,P,Q st
  P = {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} &
  Q = {qc where qc is Point of TOP-REAL 2:
  not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} holds P misses Q
proof
  let s1,t1,s2,t2,P,Q;
  assume that
A1: P= {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} and
A2: Q= {qc where qc is Point of TOP-REAL 2:
  not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)};
A3: P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by A1,Th27;
  Q= {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by A2,Th28;
  hence thesis by A3,Th26;
end;

theorem Th36:
  for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
  P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
  p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
  P1 = {pa where pa is Point of TOP-REAL 2:
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} &
  P2 = {pb where pb is Point of TOP-REAL 2:
  not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
  P`= P1 \/ P2 & P`<> {} & P1 misses P2 &
  for P1A,P2B being Subset of (TOP-REAL 2)|P` st P1A = P1 & P2B = P2 holds
  P1A is a_component & P2B is a_component
proof
  let s1,t1,s2,t2;
  let P,P1,P2 be Subset of TOP-REAL 2;
  assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P ={p where p is Point of TOP-REAL 2:p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
  p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2:
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} and
A5: P2 = {pc where pc is Point of TOP-REAL 2:
  not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2)};
  now
    let x be set;
    assume
A6: x in P`;
    then
A7: not x in P by XBOOLE_0:def 5;
    reconsider pd=x as Point of TOP-REAL 2 by A6;
    not (pd`1 = s1 & pd`2 <= t2 & pd`2 >= t1 or
    pd`1 <= s2 & pd`1 >= s1 & pd`2 = t2 or
    pd`1 <= s2 & pd`1 >= s1 & pd`2 = t1 or
    pd`1 = s2 & pd`2 <= t2 & pd`2 >= t1)by A3,A7;
    then s1<pd`1 & pd`1<s2 & t1 <pd`2 & pd`2 < t2
    or not( s1<=pd`1 & pd`1<=s2 & t1<=pd`2 & pd`2<=t2) by XXREAL_0:1;
    then x in P1 or x in P2 by A4,A5;
    hence x in P1 \/ P2 by XBOOLE_0:def 3;
  end;
  then
A8: P` c= P1 \/ P2 by TARSKI:def 3;
  now
    let x be set such that
A9: x in P1 \/ P2;
    now per cases by A9,XBOOLE_0:def 3;
      suppose
A10:    x in P1;
        then
A11:    ex pa st pa=x & s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A4;
        now
          assume x in P;
          then ex pb st pb=x &(pb`1 = s1 & pb`2 <= t2 & pb`2 >= t1 or
          pb`1 <= s2 & pb`1 >= s1 & pb`2 = t2 or
          pb`1 <= s2 & pb`1 >= s1 & pb`2 = t1 or
          pb`1 = s2 & pb`2 <= t2 & pb`2 >= t1) by A3;
          hence contradiction by A11;
        end;
        hence x in P` by A10,SUBSET_1:29;
      end;
      suppose x in P2;
        then consider pc being Point of TOP-REAL 2 such that
A12:    pc=x and
A13:    not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2) by A5;
        now
          assume pc in P;
          then ex p being Point of TOP-REAL 2 st p=pc & (
          p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
          p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
          p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
          p`1 = s2 & p`2 <= t2 & p`2 >= t1) by A3;
          hence contradiction by A1,A2,A13;
        end;
        hence x in P`by A12,SUBSET_1:29;
      end;
    end;
    hence x in P`;
  end;
  then
A14: P1 \/ P2 c= P` by TARSKI:def 3;
  hence
A15: P`=P1 \/ P2 by A8,XBOOLE_0:def 10;
  set s3 =(s1+s2)/2, t3=(t1+t2)/2;
A16: s1+s1<s1+s2 by A1,XREAL_1:6;
A17: t1+t1<t1+t2 by A2,XREAL_1:6;
A18: (s1+s1)/2<s3 by A16,XREAL_1:74;
A19: (t1+t1)/2<t3 by A17,XREAL_1:74;
A20: s1+s2<s2+s2 by A1,XREAL_1:6;
A21: t1+t2<t2+t2 by A2,XREAL_1:6;
A22: s3<(s2+s2)/2 by A20,XREAL_1:74;
A23: t3<(t2+t2)/2 by A21,XREAL_1:74;
  set pp=|[s3,t3]|;
A24: pp`1=s3 by EUCLID:52;
  pp`2=t3 by EUCLID:52;
  then
A25: |[ s3,t3 ]| in { pp2 where pp2 is Point of TOP-REAL 2:
  s1<pp2`1 & pp2`1<s2 & t1<pp2`2 & pp2`2<t2} by A18,A19,A22,A23,A24;
  hence
  P`<>{} by A4,A14;
  set P9 = P`;
  P1 misses P2 by A4,A5,Th35;
  hence
A26: P1 /\ P2 = {} by XBOOLE_0:def 7;
  now
    let P1A,P2B be Subset of (TOP-REAL 2)|P9;
    assume that
A27: P1A=P1 and
A28: P2B=P2;
    P1 is convex by A4,Th31;
    then
A29: P1A is connected by A27,CONNSP_1:23;
A30: P2 is connected by A5,Th32;
A31: P2={ |[ sa,ta ]|:not (s1<=sa & sa<=s2 & t1<=ta & ta<=t2)} by A5,Th28;
    reconsider A0={ |[ s3a,t3a ]|:s3a<s1} as Subset of TOP-REAL 2 by Lm2,Lm3;
    reconsider A1={ |[ s4,t4 ]|:t4<t1} as Subset of TOP-REAL 2 by Lm2,Lm4;
    reconsider A2={ |[ s5,t5 ]|:s2<s5} as Subset of TOP-REAL 2 by Lm2,Lm5;
    reconsider A3={ |[ s6,t6 ]|:t2<t6} as Subset of TOP-REAL 2 by Lm2,Lm6;
A32: P2=A0 \/ A1 \/ A2 \/ A3 by A31,Th8;
    t2+1>t2 by XREAL_1:29;
    then
A33: |[s2+1,t2+1]| in A3;
A34: P2B is connected by A28,A30,CONNSP_1:23;
A35: for CP being Subset of (TOP-REAL 2)|(P9) st
    CP is connected holds P1A c= CP implies P1A = CP
    proof
      let CP be Subset of (TOP-REAL 2)|(P9);
      assume CP is connected;
      then
A36:  ((TOP-REAL 2)|P9)|CP is connected by CONNSP_1:def 3;
      now
        assume
A37:    P1A c= CP;
        P1A /\ CP c= CP by XBOOLE_1:17;
        then reconsider AP=P1A /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A38:    P1 /\ P` =P1A by A15,A27,XBOOLE_1:21;
        P1 is open by A4,Th33;
        then
A39:    P1 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
A40:    P`= [#]((TOP-REAL 2)|P9) by PRE_TOPC:def 5;
        P1 /\ [#]((TOP-REAL 2)|P9)=P1A by A38,PRE_TOPC:def 5;
        then
A41:    P1A in the topology of (TOP-REAL 2)|P9 by A39,PRE_TOPC:def 4;
A42:    CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
A43:    AP<>{}(((TOP-REAL 2)|P9)|CP) by A4,A25,A27,A37,XBOOLE_1:28;
        AP in the topology of ((TOP-REAL 2)|P9)|CP by A41,A42,PRE_TOPC:def 4;
        then
A44:    AP is open by PRE_TOPC:def 2;
        P2B /\ CP c= CP by XBOOLE_1:17;
        then reconsider BP=P2B /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A45:    P2 /\ P` =P2B by A15,A28,XBOOLE_1:21;
        P2 is open by A5,Th34;
        then
A46:    P2 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
        P2 /\ [#]((TOP-REAL 2)|P9)=P2B by A45,PRE_TOPC:def 5;
        then
A47:    P2B in the topology of (TOP-REAL 2)|P9 by A46,PRE_TOPC:def 4;
        CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
        then BP in the topology of ((TOP-REAL 2)|P9)|CP by A47,PRE_TOPC:def 4;
        then
A48:    BP is open by PRE_TOPC:def 2;
A49:    CP=(P1A \/ P2B) /\ CP by A15,A27,A28,A40,XBOOLE_1:28
          .=AP \/ BP by XBOOLE_1:23;
        now
          assume
A50:      BP<>{};
A51:      AP /\ BP = P1A /\ (P2B /\ CP) /\ CP by XBOOLE_1:16
            .= P1A /\ P2B /\ CP /\ CP by XBOOLE_1:16
            .= P1A /\ P2B /\ (CP /\ CP) by XBOOLE_1:16
            .= P1A /\ P2B /\ CP;
          P1 misses P2 by A4,A5,Th35;
          then P1 /\ P2 = {} by XBOOLE_0:def 7;
          then AP misses BP by A27,A28,A51,XBOOLE_0:def 7;
          hence contradiction by A36,A42,A43,A44,A48,A49,A50,CONNSP_1:11;
        end;
        hence thesis by A49,XBOOLE_1:28;
      end;
      hence thesis;
    end;
    hence P1A is a_component by A29,CONNSP_1:def 5;
    for CP being Subset of (TOP-REAL 2)|(P9) st
    CP is connected holds P2B c= CP implies P2B = CP
    proof
      let CP be Subset of (TOP-REAL 2)|(P9);
      assume CP is connected;
      then
A52:  ((TOP-REAL 2)|P9)|CP is connected by CONNSP_1:def 3;
      assume
A53:  P2B c= CP;
      P2B /\ CP c= CP by XBOOLE_1:17;
      then reconsider BP=P2B /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A54:  P2 /\ P` =P2B by A15,A28,XBOOLE_1:21;
      P2 is open by A5,Th34;
      then
A55:  P2 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
A56:  P`= [#]((TOP-REAL 2)|P9) by PRE_TOPC:def 5;
      P2 /\ [#]((TOP-REAL 2)|P9)=P2B by A54,PRE_TOPC:def 5;
      then
A57:  P2B in the topology of (TOP-REAL 2)|P9 by A55,PRE_TOPC:def 4;
A58:  CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
A59:  BP<>{}(((TOP-REAL 2)|P9)|CP) by A28,A32,A33,A53,XBOOLE_1:28;
      BP in the topology of ((TOP-REAL 2)|P9)|CP by A57,A58,PRE_TOPC:def 4;
      then
A60:  BP is open by PRE_TOPC:def 2;
      P1A /\ CP c= CP by XBOOLE_1:17;
      then reconsider AP=P1A /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A61:  P1 /\ P` =P1A by A15,A27,XBOOLE_1:21;
      P1 is open by A4,Th33;
      then
A62:  P1 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
      P1 /\ [#]((TOP-REAL 2)|P9)=P1A by A61,PRE_TOPC:def 5;
      then
A63:  P1A in the topology of (TOP-REAL 2)|P9 by A62,PRE_TOPC:def 4;
      CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
      then AP in the topology of ((TOP-REAL 2)|P9)|CP by A63,PRE_TOPC:def 4;
      then
A64:  AP is open by PRE_TOPC:def 2;
A65:  CP=(P1A \/ P2B) /\ CP by A15,A27,A28,A56,XBOOLE_1:28
        .=AP \/ BP by XBOOLE_1:23;
      now
        assume
A66:    AP<>{};
        AP /\ BP = P1A /\ (P2B /\ CP) /\ CP by XBOOLE_1:16
          .= P1A /\ P2B /\ CP /\ CP by XBOOLE_1:16
          .= P1A /\ P2B /\ (CP /\ CP) by XBOOLE_1:16
          .= P1A /\ P2B /\ CP;
        then AP misses BP by A26,A27,A28,XBOOLE_0:def 7;
        hence contradiction by A52,A58,A59,A60,A64,A65,A66,CONNSP_1:11;
      end;
      hence thesis by A53,A65,XBOOLE_1:28;
    end;
    hence P1A is a_component &
    P2B is a_component by A29,A34,A35,CONNSP_1:def 5;
  end;
  hence thesis;
end;

Lm10: for s1,t1,s2,t2 for P,P1 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} & P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds Cl P1 = P \/ P1
proof
  let s1,t1,s2,t2;
  let P,P1 be Subset of TOP-REAL 2;
  assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
  >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
  or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa
  `2 & pa`2 < t2};
  reconsider P2 = {pb where pb is Point of TOP-REAL 2:
  not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} as Subset of TOP-REAL 2
  by Th30;
A5: P1 c= Cl P1 by PRE_TOPC:18;
  reconsider PP = P` as Subset of TOP-REAL 2;
A6: PP=P1 \/ P2 by A1,A2,A3,A4,Th36;
  P1 misses P2 by A1,A2,A3,A4,Th36;
  then
A7: P1 c= P2` by SUBSET_1:23;
  P= (P1 \/ P2)` by A6;
  then
A8: P=([#](TOP-REAL 2)\P1) /\ ([#](TOP-REAL 2)\P2) by XBOOLE_1:53;
  [#](TOP-REAL 2)=P \/ (P1 \/ P2) by A6,PRE_TOPC:2;
  then
A9: [#](TOP-REAL 2)=P \/ P1 \/ P2 by XBOOLE_1:4;
  now
    let x be set;
    assume
A10: x in P2`;
    then not x in P2 by XBOOLE_0:def 5;
    hence x in P \/ P1 by A9,A10,XBOOLE_0:def 3;
  end;
  then
A11: P2` c=P \/ P1 by TARSKI:def 3;
  now
    let x be set;
    assume x in P \/ P1;
    then x in P or x in P1 by XBOOLE_0:def 3;
    hence x in P2` by A7,A8,XBOOLE_0:def 4;
  end;
  then P \/ P1 c=P2` by TARSKI:def 3;
  then
A12: P2`= P \/ P1 by A11,XBOOLE_0:def 10;
A13: P2 is open by Th34;
  [#](TOP-REAL 2) \ P2` = P2`` .=P2;
  then
A14: P \/ P1 is closed by A12,A13,PRE_TOPC:def 3;
A15: P1 c= P \/ P1 by XBOOLE_1:7;
  thus Cl P1 c= P \/ P1
  proof
    let x be set;
    assume x in Cl P1;
    hence thesis by A14,A15,PRE_TOPC:15;
  end;
  P c= Cl P1
  proof
    let x be set;
    assume x in P;
    then consider p being Point of TOP-REAL 2 such that
A16: p=x and
A17: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
    p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
    p`1 = s2 & p`2 <= t2 & p`2 >= t1 by A3;
    reconsider q=p as Point of Euclid 2 by EUCLID:22;
    now per cases by A17;
      suppose
A18:    p`1 = s1 & p`2 <= t2 & p`2 >= t1;
        now per cases by A18,XXREAL_0:1;
          suppose
A19:        p`1 = s1 & p`2 < t2 & p`2 > t1;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A20:          Q is open and
A21:          p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A20,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A22:          r>0 and
A23:          Ball(q,r) c= Q by A21,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A24:          r/2>0 by A22,XREAL_1:215;
A25:          r/2<r by A22,XREAL_1:216;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A26:          r2 <= r/2 by XXREAL_0:17;
A27:          r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
              min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
              then
A28:          r2<=(s2-s1)/2 by A27,XXREAL_0:2;
A29:          r2<r by A25,A26,XXREAL_0:2;
A30:          s2-s1>0 by A1,XREAL_1:50;
A31:          t2-t1>0 by A2,XREAL_1:50;
A32:          (s2-s1)/2 >0 by A30,XREAL_1:215;
              (t2-t1)/2>0 by A31,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A32,XXREAL_0:15;
              then
A33:          0<r2 by A24,XXREAL_0:15;
              set pa=|[p`1+r2,p`2]|;
A34:          pa`1=p`1+r2 by EUCLID:52;
A35:          pa`2=p`2 by EUCLID:52;
              (s2-s1)/2<s2-s1 by A30,XREAL_1:216;
              then
A36:          r2<s2-p`1 by A19,A28,XXREAL_0:2;
A37:          s1<pa`1 by A19,A33,A34,XREAL_1:29;
              pa`1<s2 by A34,A36,XREAL_1:20;
              then
A38:          pa in P1 by A4,A19,A35,A37;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A39:          0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A40:          0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A39,XREAL_1:7;
              (pa`1-p`1)^2=(p`1-pa`1)^2;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
              by A29,A33,A34,A35,SQUARE_1:16;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A40,SQUARE_1:def 2;
              then
A41:          sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A22,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A41,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A23,A38,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
          suppose
A42:        p`1 = s1 & p`2 = t1;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A43:          Q is open and
A44:          p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A43,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A45:          r>0 and
A46:          Ball(q,r) c= Q by A44,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A47:          r/2>0 by A45,XREAL_1:215;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A48:          r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A49:          min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A50:          min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A51:          r2<=(s2-s1)/2 by A48,A49,XXREAL_0:2;
A52:          r2<= (t2-t1)/2 by A48,A50,XXREAL_0:2;
A53:          s2-s1>0 by A1,XREAL_1:50;
A54:          t2-t1>0 by A2,XREAL_1:50;
A55:          (s2-s1)/2 >0 by A53,XREAL_1:215;
              (t2-t1)/2>0 by A54,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A55,XXREAL_0:15;
              then
A56:          0<r2 by A47,XXREAL_0:15;
              set pa=|[p`1+r2,p`2+r2]|;
A57:          pa`1=p`1+r2 by EUCLID:52;
A58:          pa`2=p`2+r2 by EUCLID:52;
A59:          pa`1> s1 by A42,A56,A57,XREAL_1:29;
A60:          pa`2> t1 by A42,A56,A58,XREAL_1:29;
              (s2-s1)/2<s2-s1 by A53,XREAL_1:216;
              then r2<s2-p`1 by A42,A51,XXREAL_0:2;
              then
A61:          pa`1<s2 by A57,XREAL_1:20;
              (t2-t1)/2<t2-t1 by A54,XREAL_1:216;
              then r2<t2-p`2 by A42,A52,XXREAL_0:2;
              then pa`2<t2 by A58,XREAL_1:20;
              then
A62:          pa in P1 by A4,A59,A60,A61;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A63:          0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A64:          0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A63,XREAL_1:7;
              (pa`1-p`1)^2=(p`1-pa`1)^2;
then (p`1 - pa`1)^2 <= (r/2)^2 by A56,A57,SQUARE_1:15,XXREAL_0:17;
              then
              A65:          (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
              by A57,A58,XREAL_1:7;
              r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
              then r^2>(r/2)^2+(r/2)^2 by A45,A47,XREAL_1:29,129;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A65,XXREAL_0:2;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A64,SQUARE_1:def 2;
              then
A66:          sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A45,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A66,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A46,A62,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
          suppose
A67:        p`1 = s1 & p`2 = t2;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A68:          Q is open and
A69:          p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A68,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A70:          r>0 and
A71:          Ball(q,r) c= Q by A69,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A72:          r/2>0 by A70,XREAL_1:215;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A73:          r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A74:          min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A75:          min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A76:          r2<=(s2-s1)/2 by A73,A74,XXREAL_0:2;
A77:          r2<= (t2-t1)/2 by A73,A75,XXREAL_0:2;
A78:          s2-s1>0 by A1,XREAL_1:50;
A79:          t2-t1>0 by A2,XREAL_1:50;
A80:          (s2-s1)/2 >0 by A78,XREAL_1:215;
              (t2-t1)/2>0 by A79,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A80,XXREAL_0:15;
              then
A81:          0<r2 by A72,XXREAL_0:15;
              set pa=|[p`1+r2,p`2-r2]|;
A82:          pa`1=p`1+r2 by EUCLID:52;
A83:          pa`2=p`2-r2 by EUCLID:52;
A84:          pa`1> s1 by A67,A81,A82,XREAL_1:29;
A85:          pa`2< t2 by A67,A81,A83,XREAL_1:44;
              (s2-s1)/2<s2-s1 by A78,XREAL_1:216;
              then r2<s2-p`1 by A67,A76,XXREAL_0:2;
              then
A86:          pa`1<s2 by A82,XREAL_1:20;
              (t2-t1)/2<t2-t1 by A79,XREAL_1:216;
              then r2<p`2-t1 by A67,A77,XXREAL_0:2;
              then pa`2>t1 by A83,XREAL_1:12;
              then
A87:          pa in P1 by A4,A84,A85,A86;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A88:          0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A89:          0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A88,XREAL_1:7;
              r2^2<= (r/2)^2 by A81,SQUARE_1:15,XXREAL_0:17;
              then
              A90:          (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
              by A82,A83,XREAL_1:7;
              r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
              then r^2>(r/2)^2+(r/2)^2 by A70,A72,XREAL_1:29,129;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A90,XXREAL_0:2;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A89,SQUARE_1:def 2;
              then
A91:          sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A70,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A91,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A71,A87,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
        end;
        hence thesis by A16;
      end;
      suppose
A92:    p`1 <= s2 & p`1 >= s1 & p`2 = t2;
        now per cases by A92,XXREAL_0:1;
          suppose
A93:        p`2 = t2 & p`1 < s2 & p`1 > s1;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A94:          Q is open and
A95:          p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A94,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A96:          r>0 and
A97:          Ball(q,r) c= Q by A95,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A98:          r/2>0 by A96,XREAL_1:215;
A99:          r/2<r by A96,XREAL_1:216;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A100:         r2 <= r/2 by XXREAL_0:17;
A101:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
              min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
              then
A102:         r2<= (t2-t1)/2 by A101,XXREAL_0:2;
A103:         r2<r by A99,A100,XXREAL_0:2;
A104:         s2-s1>0 by A1,XREAL_1:50;
A105:         t2-t1>0 by A2,XREAL_1:50;
A106:         (s2-s1)/2 >0 by A104,XREAL_1:215;
              (t2-t1)/2>0 by A105,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A106,XXREAL_0:15;
              then
A107:         0<r2 by A98,XXREAL_0:15;
              set pa=|[p`1,p`2-r2]|;
A108:         pa`1=p`1 by EUCLID:52;
A109:         pa`2=p`2-r2 by EUCLID:52;
              (t2-t1)/2<t2-t1 by A105,XREAL_1:216;
              then r2<p`2-t1 by A93,A102,XXREAL_0:2;
              then
A110:         t1 <pa`2 by A109,XREAL_1:12;
              pa`2 < t2 by A93,A107,A109,XREAL_1:44;
              then
A111:         pa in P1 by A4,A93,A108,A110;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A112:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A113:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A112,XREAL_1:7;
              (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
              by A103,A107,A108,A109,SQUARE_1:16;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A113,SQUARE_1:def 2;
              then
A114:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A96,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A114,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A97,A111,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
          suppose
A115:       p`2 = t2 & p`1 = s1;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A116:         Q is open and
A117:         p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A116,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A118:         r>0 and
A119:         Ball(q,r) c= Q by A117,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A120:         r/2>0 by A118,XREAL_1:215;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A121:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A122:         min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A123:         min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A124:         r2<=(s2-s1)/2 by A121,A122,XXREAL_0:2;
A125:         r2<= (t2-t1)/2 by A121,A123,XXREAL_0:2;
A126:         s2-s1>0 by A1,XREAL_1:50;
A127:         t2-t1>0 by A2,XREAL_1:50;
A128:         (s2-s1)/2 >0 by A126,XREAL_1:215;
              (t2-t1)/2>0 by A127,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A128,XXREAL_0:15;
              then
A129:         0<r2 by A120,XXREAL_0:15;
              set pa=|[p`1+r2,p`2-r2]|;
A130:         pa`1=p`1+r2 by EUCLID:52;
A131:         pa`2=p`2-r2 by EUCLID:52;
A132:         pa`1> s1 by A115,A129,A130,XREAL_1:29;
A133:         pa`2< t2 by A115,A129,A131,XREAL_1:44;
              (t2-t1)/2<t2-t1 by A127,XREAL_1:216;
              then r2<p`2-t1 by A115,A125,XXREAL_0:2;
              then
A134:         pa`2>t1 by A131,XREAL_1:12;
              (s2-s1)/2<s2-s1 by A126,XREAL_1:216;
              then r2<s2-p`1 by A115,A124,XXREAL_0:2;
              then pa`1<s2 by A130,XREAL_1:20;
              then
A135:         pa in P1 by A4,A132,A133,A134;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A136:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A137:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A136,XREAL_1:7;
              (p`2 - pa`2)^2 <= (r/2)^2 by A129,A131,SQUARE_1:15,XXREAL_0:17;
              then
              A138:         (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
              by A130,A131,XREAL_1:7;
              r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
              then r^2>(r/2)^2+(r/2)^2 by A118,A120,XREAL_1:29,129;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A138,XXREAL_0:2;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A137,SQUARE_1:def 2;
              then
A139:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A118,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A139,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A119,A135,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
          suppose
A140:       p`2 = t2 & p`1 = s2;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A141:         Q is open and
A142:         p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A141,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A143:         r>0 and
A144:         Ball(q,r) c= Q by A142,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A145:         r/2>0 by A143,XREAL_1:215;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A146:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A147:         min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A148:         min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A149:         r2<=(s2-s1)/2 by A146,A147,XXREAL_0:2;
A150:         r2<= (t2-t1)/2 by A146,A148,XXREAL_0:2;
A151:         s2-s1>0 by A1,XREAL_1:50;
A152:         t2-t1>0 by A2,XREAL_1:50;
A153:         (s2-s1)/2 >0 by A151,XREAL_1:215;
              (t2-t1)/2>0 by A152,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A153,XXREAL_0:15;
              then
A154:         0<r2 by A145,XXREAL_0:15;
              set pa=|[p`1-r2,p`2-r2]|;
A155:         pa`1=p`1-r2 by EUCLID:52;
A156:         pa`2=p`2-r2 by EUCLID:52;
A157:         pa`1< s2 by A140,A154,A155,XREAL_1:44;
A158:         pa`2< t2 by A140,A154,A156,XREAL_1:44;
              (s2-s1)/2<s2-s1 by A151,XREAL_1:216;
              then r2<p`1-s1 by A140,A149,XXREAL_0:2;
              then
A159:         pa`1>s1 by A155,XREAL_1:12;
              (t2-t1)/2<t2-t1 by A152,XREAL_1:216;
              then r2<p`2-t1 by A140,A150,XXREAL_0:2;
              then pa`2>t1 by A156,XREAL_1:12;
              then
A160:         pa in P1 by A4,A157,A158,A159;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A161:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A162:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A161,XREAL_1:7;
              r2^2<= (r/2)^2 by A154,SQUARE_1:15,XXREAL_0:17;
              then
              A163:         (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
              by A155,A156,XREAL_1:7;
              r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
              then r^2>(r/2)^2+(r/2)^2 by A143,A145,XREAL_1:29,129;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A163,XXREAL_0:2;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A162,SQUARE_1:def 2;
              then
A164:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A143,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A164,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A144,A160,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
        end;
        hence thesis by A16;
      end;
      suppose
A165:   p`1 <= s2 & p`1 >= s1 & p`2 = t1;
        now per cases by A165,XXREAL_0:1;
          suppose
A166:       p`2 = t1 & p`1 < s2 & p`1 > s1;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A167:         Q is open and
A168:         p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A167,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A169:         r>0 and
A170:         Ball(q,r) c= Q by A168,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A171:         r/2>0 by A169,XREAL_1:215;
A172:         r/2<r by A169,XREAL_1:216;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A173:         r2 <= r/2 by XXREAL_0:17;
A174:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
              min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
              then
A175:         r2<= (t2-t1)/2 by A174,XXREAL_0:2;
A176:         r2<r by A172,A173,XXREAL_0:2;
A177:         s2-s1>0 by A1,XREAL_1:50;
A178:         t2-t1>0 by A2,XREAL_1:50;
A179:         (s2-s1)/2 >0 by A177,XREAL_1:215;
              (t2-t1)/2>0 by A178,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A179,XXREAL_0:15;
              then
A180:         0<r2 by A171,XXREAL_0:15;
              set pa=|[p`1,p`2+r2]|;
A181:         pa`2=p`2+r2 by EUCLID:52;
A182:         pa`1=p`1 by EUCLID:52;
              (t2-t1)/2<t2-t1 by A178,XREAL_1:216;
              then
A183:         r2<t2-p`2 by A166,A175,XXREAL_0:2;
A184:         t1 <pa`2 by A166,A180,A181,XREAL_1:29;
              pa`2 < t2 by A181,A183,XREAL_1:20;
              then
A185:         pa in P1 by A4,A166,A182,A184;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A186:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A187:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A186,XREAL_1:7;
              (pa`2-p`2)^2=(p`2-pa`2)^2;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A176,A180,A181,A182
,SQUARE_1:16;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A187,SQUARE_1:def 2;
              then
A188:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A169,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A188,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A170,A185,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
          suppose
A189:       p`2 = t1 & p`1 = s1;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A190:         Q is open and
A191:         p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A190,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A192:         r>0 and
A193:         Ball(q,r) c= Q by A191,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A194:         r/2>0 by A192,XREAL_1:215;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A195:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A196:         min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A197:         min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A198:         r2<=(s2-s1)/2 by A195,A196,XXREAL_0:2;
A199:         r2<= (t2-t1)/2 by A195,A197,XXREAL_0:2;
A200:         s2-s1>0 by A1,XREAL_1:50;
A201:         t2-t1>0 by A2,XREAL_1:50;
A202:         (s2-s1)/2 >0 by A200,XREAL_1:215;
              (t2-t1)/2>0 by A201,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A202,XXREAL_0:15;
              then
A203:         0<r2 by A194,XXREAL_0:15;
              set pa=|[p`1+r2,p`2+r2]|;
A204:         pa`1=p`1+r2 by EUCLID:52;
A205:         pa`2=p`2+r2 by EUCLID:52;
A206:         pa`1> s1 by A189,A203,A204,XREAL_1:29;
A207:         pa`2> t1 by A189,A203,A205,XREAL_1:29;
              (s2-s1)/2<s2-s1 by A200,XREAL_1:216;
              then r2<s2-p`1 by A189,A198,XXREAL_0:2;
              then
A208:         pa`1<s2 by A204,XREAL_1:20;
              (t2-t1)/2<t2-t1 by A201,XREAL_1:216;
              then r2<t2-p`2 by A189,A199,XXREAL_0:2;
              then pa`2<t2 by A205,XREAL_1:20;
              then
A209:         pa in P1 by A4,A206,A207,A208;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A210:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A211:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A210,XREAL_1:7;
              (pa`1-p`1)^2=(p`1-pa`1)^2;
then (p`1 - pa`1)^2 <= (r/2)^2 by A203,A204,SQUARE_1:15,XXREAL_0:17;
              then
              A212:         (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
              by A204,A205,XREAL_1:7;
              r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
              then r^2>(r/2)^2+(r/2)^2 by A192,A194,XREAL_1:29,129;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A212,XXREAL_0:2;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A211,SQUARE_1:def 2;
              then
A213:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A192,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A213,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A193,A209,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
          suppose
A214:       p`2 = t1 & p`1 = s2;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A215:         Q is open and
A216:         p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A215,Lm9,PRE_TOPC:30;
              then consider r be real number such that
A217:         r>0 and
A218:         Ball(q,r) c= Q by A216,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A219:         r/2>0 by A217,XREAL_1:215;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A220:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A221:         min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A222:         min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A223:         r2<=(s2-s1)/2 by A220,A221,XXREAL_0:2;
A224:         r2<= (t2-t1)/2 by A220,A222,XXREAL_0:2;
A225:         s2-s1>0 by A1,XREAL_1:50;
A226:         t2-t1>0 by A2,XREAL_1:50;
A227:         (s2-s1)/2 >0 by A225,XREAL_1:215;
              (t2-t1)/2>0 by A226,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A227,XXREAL_0:15;
              then
A228:         0<r2 by A219,XXREAL_0:15;
              set pa=|[p`1-r2,p`2+r2]|;
A229:         pa`1=p`1-r2 by EUCLID:52;
A230:         pa`2=p`2+r2 by EUCLID:52;
              then
A231:         pa`2> t1 by A214,A228,XREAL_1:29;
A232:         pa`1< s2 by A214,A228,A229,XREAL_1:44;
              (t2-t1)/2<t2-t1 by A226,XREAL_1:216;
              then r2<t2-p`2 by A214,A224,XXREAL_0:2;
              then
A233:         pa`2<t2 by A230,XREAL_1:20;
              (s2-s1)/2<s2-s1 by A225,XREAL_1:216;
              then r2<p`1-s1 by A214,A223,XXREAL_0:2;
              then pa`1>s1 by A229,XREAL_1:12;
              then
A234:         pa in P1 by A4,A231,A232,A233;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A235:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A236:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A235,XREAL_1:7;
              r2^2<= (r/2)^2 by A228,SQUARE_1:15,XXREAL_0:17;
              then
              A237:         (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
              by A229,A230,XREAL_1:7;
              r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
              then r^2>(r/2)^2+(r/2)^2 by A217,A219,XREAL_1:29,129;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A237,XXREAL_0:2;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A236,SQUARE_1:def 2;
              then
A238:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A217,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A238,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A218,A234,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
        end;
        hence thesis by A16;
      end;
      suppose
A239:   p`1 = s2 & p`2 <= t2 & p`2 >= t1;
        now per cases by A239,XXREAL_0:1;
          suppose
A240:       p`1 = s2 & p`2 < t2 & p`2 > t1;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A241:         Q is open and
A242:         p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A241,Lm9,PRE_TOPC:30;
              then consider r being real number such that
A243:         r>0 and
A244:         Ball(q,r) c= Q by A242,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A245:         r/2>0 by A243,XREAL_1:215;
A246:         r/2<r by A243,XREAL_1:216;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A247:         r2 <= r/2 by XXREAL_0:17;
A248:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
              min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
              then
A249:         r2<=(s2-s1)/2 by A248,XXREAL_0:2;
A250:         r2<r by A246,A247,XXREAL_0:2;
A251:         s2-s1>0 by A1,XREAL_1:50;
A252:         t2-t1>0 by A2,XREAL_1:50;
A253:         (s2-s1)/2 >0 by A251,XREAL_1:215;
              (t2-t1)/2>0 by A252,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A253,XXREAL_0:15;
              then
A254:         0<r2 by A245,XXREAL_0:15;
              set pa=|[p`1-r2,p`2]|;
A255:         pa`2=p`2 by EUCLID:52;
A256:         pa`1=p`1-r2 by EUCLID:52;
              (s2-s1)/2<s2-s1 by A251,XREAL_1:216;
              then r2<p`1-s1 by A240,A249,XXREAL_0:2;
              then
A257:         s1<pa`1 by A256,XREAL_1:12;
              pa`1<s2 by A240,A254,A256,XREAL_1:44;
              then
A258:         pa in P1 by A4,A240,A255,A257;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A259:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A260:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A259,XREAL_1:7;
              (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
              by A250,A254,A255,A256,SQUARE_1:16;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A260,SQUARE_1:def 2;
              then
A261:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A243,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A261,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A244,A258,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
          suppose
A262:       p`1 = s2 & p`2 = t1;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A263:         Q is open and
A264:         p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A263,Lm9,PRE_TOPC:30;
              then consider r being real number such that
A265:         r>0 and
A266:         Ball(q,r) c= Q by A264,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A267:         r/2>0 by A265,XREAL_1:215;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A268:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A269:         min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A270:         min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A271:         r2<=(s2-s1)/2 by A268,A269,XXREAL_0:2;
A272:         r2<= (t2-t1)/2 by A268,A270,XXREAL_0:2;
A273:         s2-s1>0 by A1,XREAL_1:50;
A274:         t2-t1>0 by A2,XREAL_1:50;
A275:         (s2-s1)/2 >0 by A273,XREAL_1:215;
              (t2-t1)/2>0 by A274,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A275,XXREAL_0:15;
              then
A276:         0<r2 by A267,XXREAL_0:15;
              set pa=|[p`1-r2,p`2+r2]|;
A277:         pa`2=p`2+r2 by EUCLID:52;
A278:         pa`1=p`1-r2 by EUCLID:52;
A279:         pa`2> t1 by A262,A276,A277,XREAL_1:29;
A280:         pa`1< s2 by A262,A276,A278,XREAL_1:44;
              (s2-s1)/2<s2-s1 by A273,XREAL_1:216;
              then r2<p`1-s1 by A262,A271,XXREAL_0:2;
              then
A281:         pa`1>s1 by A278,XREAL_1:12;
              (t2-t1)/2<t2-t1 by A274,XREAL_1:216;
              then r2<t2-p`2 by A262,A272,XXREAL_0:2;
              then pa`2<t2 by A277,XREAL_1:20;
              then
A282:         pa in P1 by A4,A279,A280,A281;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A283:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A284:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A283,XREAL_1:7;
              (p`1 - pa`1)^2 <= (r/2)^2 by A276,A278,SQUARE_1:15,XXREAL_0:17;
              then
              A285:         (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
              by A277,A278,XREAL_1:7;
              r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
              then r^2>(r/2)^2+(r/2)^2 by A265,A267,XREAL_1:29,129;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A285,XXREAL_0:2;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A284,SQUARE_1:def 2;
              then
A286:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A265,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A286,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A266,A282,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
          suppose
A287:       p`1 = s2 & p`2 = t2;
            for Q being Subset of TOP-REAL 2 st Q is open holds
            p in Q implies P1 meets Q
            proof
              let Q be Subset of TOP-REAL 2;
              assume that
A288:         Q is open and
A289:         p in Q;
              reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
              QQ is open by A288,Lm9,PRE_TOPC:30;
              then consider r being real number such that
A290:         r>0 and
A291:         Ball(q,r) c= Q by A289,TOPMETR:15;
              reconsider r as Real by XREAL_0:def 1;
A292:         r/2>0 by A290,XREAL_1:215;
              set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A293:         r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A294:         min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A295:         min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A296:         r2<=(s2-s1)/2 by A293,A294,XXREAL_0:2;
A297:         r2<= (t2-t1)/2 by A293,A295,XXREAL_0:2;
A298:         s2-s1>0 by A1,XREAL_1:50;
A299:         t2-t1>0 by A2,XREAL_1:50;
A300:         (s2-s1)/2 >0 by A298,XREAL_1:215;
              (t2-t1)/2>0 by A299,XREAL_1:215;
              then 0<min((s2-s1)/2,(t2-t1)/2) by A300,XXREAL_0:15;
              then
A301:         0<r2 by A292,XXREAL_0:15;
              set pa=|[p`1-r2,p`2-r2]|;
A302:         pa`1=p`1-r2 by EUCLID:52;
A303:         pa`2=p`2-r2 by EUCLID:52;
A304:         pa`1< s2 by A287,A301,A302,XREAL_1:44;
A305:         pa`2< t2 by A287,A301,A303,XREAL_1:44;
              (s2-s1)/2<s2-s1 by A298,XREAL_1:216;
              then r2<p`1-s1 by A287,A296,XXREAL_0:2;
              then
A306:         pa`1>s1 by A302,XREAL_1:12;
              (t2-t1)/2<t2-t1 by A299,XREAL_1:216;
              then r2<p`2-t1 by A287,A297,XXREAL_0:2;
              then pa`2>t1 by A303,XREAL_1:12;
              then
A307:         pa in P1 by A4,A304,A305,A306;
              reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A308:         0 <= (p`1 - pa`1)^2 by XREAL_1:63;
              0 <= (p`2 - pa`2)^2 by XREAL_1:63;
              then
A309:         0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A308,XREAL_1:7;
              r2^2<= (r/2)^2 by A301,SQUARE_1:15,XXREAL_0:17;
              then
              A310:         (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
              by A302,A303,XREAL_1:7;
              r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
              then r^2>(r/2)^2+(r/2)^2 by A290,A292,XREAL_1:29,129;
              then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A310,XXREAL_0:2;
              then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
              by A309,SQUARE_1:def 2;
              then
A311:         sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A290,SQUARE_1:15;
              (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
              then dist(q,qa)<r by A311,TOPREAL3:7;
              then pa in Ball(q,r) by METRIC_1:11;
              hence thesis by A291,A307,XBOOLE_0:3;
            end;
            hence p in Cl P1 by PRE_TOPC:def 7;
          end;
        end;
        hence thesis by A16;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A5,XBOOLE_1:8;
end;

Lm11: for s1,t1,s2,t2 for P,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} & P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds Cl P2 = P \/ P2
proof
  let s1,t1,s2,t2;
  let P,P2 be Subset of TOP-REAL 2;
  assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
  >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
  or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
  t1<=pb`2 & pb`2<=t2)};
A5: P2 c= Cl P2 by PRE_TOPC:18;
  reconsider P1 = {pa where pa is Point of TOP-REAL 2:
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} as Subset of TOP-REAL 2 by Th29;
  reconsider PP = P` as Subset of TOP-REAL 2;
A6: PP=P1 \/ P2 by A1,A2,A3,A4,Th36;
  P1 misses P2 by A1,A2,A3,A4,Th36;
  then
A7: P2 c= P1` by SUBSET_1:23;
  P= (P1 \/ P2)` by A6;
  then
A8: P=([#](TOP-REAL 2)\P1) /\ ([#](TOP-REAL 2)\P2) by XBOOLE_1:53;
A9: [#](TOP-REAL 2)=P \/ (P2 \/ P1) by A6,PRE_TOPC:2
    .=P \/ P2 \/ P1 by XBOOLE_1:4;
  now
    let x be set;
    assume
A10: x in P1`;
    then not x in P1 by XBOOLE_0:def 5;
    hence x in P \/ P2 by A9,A10,XBOOLE_0:def 3;
  end;
  then
A11: P1` c=P \/ P2 by TARSKI:def 3;
  now
    let x be set;
    assume x in P \/ P2;
    then x in P or x in P2 by XBOOLE_0:def 3;
    hence x in P1` by A7,A8,XBOOLE_0:def 4;
  end;
  then P \/ P2 c=P1` by TARSKI:def 3;
  then
A12: P1`= P \/ P2 by A11,XBOOLE_0:def 10;
A13: P1 is open by Th33;
  [#](TOP-REAL 2) \ P1` = P1`` .=P1;
  then
A14: P \/ P2 is closed by A12,A13,PRE_TOPC:def 3;
A15: P2 c= P \/ P2 by XBOOLE_1:7;
  thus Cl P2 c= P \/ P2
  proof
    let x be set;
    assume x in Cl P2;
    hence thesis by A14,A15,PRE_TOPC:15;
  end;
  P c= Cl P2
  proof
    let x be set;
    assume x in P;
    then consider p being Point of TOP-REAL 2 such that
A16: p=x and
A17: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
    p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
    p`1 = s2 & p`2 <= t2 & p`2 >= t1 by A3;
    reconsider q=p as Point of Euclid 2 by EUCLID:22;
    now per cases by A17;
      suppose
A18:    p`1 = s1 & p`2 <= t2 & p`2 >= t1;
        for Q being Subset of TOP-REAL 2 st Q is open holds
        p in Q implies P2 meets Q
        proof
          let Q be Subset of TOP-REAL 2;
          assume that
A19:      Q is open and
A20:      p in Q;
          reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
          QQ is open by A19,Lm9,PRE_TOPC:30;
          then consider r be real number such that
A21:      r>0 and
A22:      Ball(q,r) c= Q by A20,TOPMETR:15;
          reconsider r as Real by XREAL_0:def 1;
          set pa=|[p`1-r/2,p`2]|;
A23:      pa`1=p`1-r/2 by EUCLID:52;
A24:      pa`2=p`2 by EUCLID:52;
A25:      r/2>0 by A21,XREAL_1:215;
          not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A18,A21,A23,
XREAL_1:44,215;
          then
A26:      pa in P2 by A4;
          reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A27:      0 <= (p`1 - pa`1)^2 by XREAL_1:63;
          0 <= (p`2 - pa`2)^2 by XREAL_1:63;
          then
A28:      0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A27,XREAL_1:7;
          p`1 - pa`1 < r by A21,A23,XREAL_1:216;
          then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A23,A24,A25,SQUARE_1:16
;
          then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
          by A28,SQUARE_1:def 2;
          then
A29:      sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A21,SQUARE_1:15;
          (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
          then dist(q,qa)<r by A29,TOPREAL3:7;
          then pa in Ball(q,r) by METRIC_1:11;
          then P2 /\ Q <> {} by A22,A26,XBOOLE_0:def 4;
          hence thesis by XBOOLE_0:def 7;
        end;
        hence thesis by A16,PRE_TOPC:def 7;
      end;
      suppose
A30:    p`1 <= s2 & p`1 >= s1 & p`2 = t2;
        for Q being Subset of TOP-REAL 2 st Q is open holds
        p in Q implies P2 meets Q
        proof
          let Q be Subset of TOP-REAL 2;
          assume that
A31:      Q is open and
A32:      p in Q;
          reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
          QQ is open by A31,Lm9,PRE_TOPC:30;
          then consider r being real number such that
A33:      r>0 and
A34:      Ball(q,r) c= Q by A32,TOPMETR:15;
          reconsider r as Real by XREAL_0:def 1;
          set pa=|[p`1,p`2+r/2]|;
A35:      pa`1=p`1 by EUCLID:52;
A36:      pa`2=p`2+r/2 by EUCLID:52;
A37:      r/2>0 by A33,XREAL_1:215;
          not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A30,A33,A36,
XREAL_1:29,215;
          then
A38:      pa in P2 by A4;
          reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A39:      0 <= (p`1 - pa`1)^2 by XREAL_1:63;
          0 <= (p`2 - pa`2)^2 by XREAL_1:63;
          then
A40:      0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A39,XREAL_1:7;
A41:      pa`2 - p`2 < r by A33,A36,XREAL_1:216;
          (pa`2-p`2)^2=(p`2-pa`2)^2;
          then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
          by A35,A36,A37,A41,SQUARE_1:16;
          then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
          by A40,SQUARE_1:def 2;
          then
A42:      sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A33,SQUARE_1:15;
          (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
          then dist(q,qa)<r by A42,TOPREAL3:7;
          then pa in Ball(q,r) by METRIC_1:11;
          then P2 /\ Q <> {} by A34,A38,XBOOLE_0:def 4;
          hence thesis by XBOOLE_0:def 7;
        end;
        hence thesis by A16,PRE_TOPC:def 7;
      end;
      suppose
A43:    p`1 <= s2 & p`1 >= s1 & p`2 = t1;
        for Q being Subset of TOP-REAL 2 st Q is open holds
        p in Q implies P2 meets Q
        proof
          let Q be Subset of TOP-REAL 2;
          assume that
A44:      Q is open and
A45:      p in Q;
          reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
          QQ is open by A44,Lm9,PRE_TOPC:30;
          then consider r being real number such that
A46:      r>0 and
A47:      Ball(q,r) c= Q by A45,TOPMETR:15;
          reconsider r as Real by XREAL_0:def 1;
          set pa=|[p`1,p`2-r/2]|;
A48:      pa`1=p`1 by EUCLID:52;
A49:      pa`2=p`2-r/2 by EUCLID:52;
A50:      r/2>0 by A46,XREAL_1:215;
          not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2)
          by A43,A46,A49,XREAL_1:44,215;
          then
A51:      pa in P2 by A4;
          reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A52:      0 <= (p`1 - pa`1)^2 by XREAL_1:63;
          0 <= (p`2 - pa`2)^2 by XREAL_1:63;
          then
A53:      0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A52,XREAL_1:7;
          p`2 - pa`2 < r by A46,A49,XREAL_1:216;
          then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A48,A49,A50,SQUARE_1:16
;
          then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
          by A53,SQUARE_1:def 2;
          then
A54:      sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A46,SQUARE_1:15;
          (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
          then dist(q,qa)<r by A54,TOPREAL3:7;
          then pa in Ball(q,r) by METRIC_1:11;
          hence thesis by A47,A51,XBOOLE_0:3;
        end;
        hence thesis by A16,PRE_TOPC:def 7;
      end;
      suppose
A55:    p`1 = s2 & p`2 <= t2 & p`2 >= t1;
        for Q being Subset of TOP-REAL 2 st Q is open holds
        p in Q implies P2 meets Q
        proof
          let Q be Subset of TOP-REAL 2;
          assume that
A56:      Q is open and
A57:      p in Q;
          reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
          QQ is open by A56,Lm9,PRE_TOPC:30;
          then consider r being real number such that
A58:      r>0 and
A59:      Ball(q,r) c= Q by A57,TOPMETR:15;
          reconsider r as Real by XREAL_0:def 1;
          set pa=|[p`1+r/2,p`2]|;
A60:      pa`1=p`1+r/2 by EUCLID:52;
A61:      pa`2=p`2 by EUCLID:52;
A62:      r/2>0 by A58,XREAL_1:215;
          not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2)
          by A55,A58,A60,XREAL_1:29,215;
          then
A63:      pa in P2 by A4;
          reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A64:      0 <= (p`1 - pa`1)^2 by XREAL_1:63;
          0 <= (p`2 - pa`2)^2 by XREAL_1:63;
          then
A65:      0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A64,XREAL_1:7;
A66:      pa`1 - p`1 < r by A58,A60,XREAL_1:216;
          (pa`1-p`1)^2=(p`1-pa`1)^2;
          then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
          by A60,A61,A62,A66,SQUARE_1:16;
          then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
          by A65,SQUARE_1:def 2;
          then
A67:      sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A58,SQUARE_1:15;
          (Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
          then dist(q,qa)<r by A67,TOPREAL3:7;
          then pa in Ball(q,r) by METRIC_1:11;
          hence thesis by A59,A63,XBOOLE_0:3;
        end;
        hence thesis by A16,PRE_TOPC:def 7;
      end;
    end;
    hence thesis;
  end;
  hence thesis by A5,XBOOLE_1:8;
end;

theorem Th37:
  for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
  P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
  p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
  P1 = {pa where pa is Point of TOP-REAL 2:
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} &
  P2 = {pb where pb is Point of TOP-REAL 2:
  not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)}
  holds P = (Cl P1) \ P1 & P = (Cl P2) \P2
proof
  let s1,t1,s2,t2;
  let P,P1,P2 be Subset of TOP-REAL 2;
  assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
  >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
  or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa
  `2 & pa`2 < t2} and
A5: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
  t1<=pb`2 & pb`2<=t2)};
  reconsider PP = P` as Subset of TOP-REAL 2;
  PP=P1 \/ P2 by A1,A2,A3,A4,A5,Th36;
  then P= (P1 \/ P2)`;
  then
A6: P=([#](TOP-REAL 2)\P1) /\ ([#](TOP-REAL 2)\P2) by XBOOLE_1:53;
  then
A7: P c=[#](TOP-REAL 2)\P2 by XBOOLE_1:17;
A8: Cl P2 = P \/ P2 by A1,A2,A3,A5,Lm11;
A9: (P \/ P2) \ P2 c= P
  proof
    let x be set;
    assume
A10: x in (P \/ P2) \ P2;
    then
A11: x in P \/ P2 by XBOOLE_0:def 5;
    not x in P2 by A10,XBOOLE_0:def 5;
    hence thesis by A11,XBOOLE_0:def 3;
  end;
  P c= Cl P2 by A8,XBOOLE_1:7;
  then P c= Cl P2 /\ P2` by A7,XBOOLE_1:19;
  then
A12: P c= (Cl P2)\P2 by SUBSET_1:13;
A13: P c=[#](TOP-REAL 2)\P1 by A6,XBOOLE_1:17;
A14: Cl P1 = P \/ P1 by A1,A2,A3,A4,Lm10;
A15: (P \/ P1) \ P1 c= P
  proof
    let x be set;
    assume
A16: x in (P \/ P1) \ P1;
    then
A17: x in P \/ P1 by XBOOLE_0:def 5;
    not x in P1 by A16,XBOOLE_0:def 5;
    hence thesis by A17,XBOOLE_0:def 3;
  end;
  P c= Cl P1 by A14,XBOOLE_1:7;
  then P c= Cl P1 /\ P1` by A13,XBOOLE_1:19;
  then P c= (Cl P1)\P1 by SUBSET_1:13;
  hence thesis by A8,A9,A12,A14,A15,XBOOLE_0:def 10;
end;

theorem Th38:
  for s1,s2,t1,t2,P,P1 st P = { p where p is Point of TOP-REAL 2:
  p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
  P1 = {pa where pa is Point of TOP-REAL 2:
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds P1 c= [#] ((TOP-REAL 2)|P`)
proof
  let s1,s2,t1,t2,P,P1;
  assume that
A1: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1
or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1
  = s2 & p`2 <= t2 & p`2 >= t1} and
A2: P1 = {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa
  `2 & pa`2 < t2};
  let x be set;
  assume
A3: x in P1;
  then
A4: ex pa being Point of TOP-REAL 2 st pa=x &
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A2;
  now
    assume x in { p where p is Point of TOP-REAL 2:
    p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
    p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
    then ex p being Point of TOP-REAL 2 st p=x & (
    p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
    p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1);
    hence contradiction by A4;
  end;
  then x in P` by A1,A3,SUBSET_1:29;
  hence thesis by PRE_TOPC:def 5;
end;

theorem
  for s1,s2,t1,t2,P,P1 st P = { p where p is Point of TOP-REAL 2:
  p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
  P1 = {pa where pa is Point of TOP-REAL 2:
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds
  P1 is Subset of (TOP-REAL 2)|P`
proof
  let s1,s2,t1,t2,P,P1;
  assume that
A1: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1
or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1
  = s2 & p`2 <= t2 & p`2 >= t1} and
A2: P1 = {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa
  `2 & pa`2 < t2};
  P1 c= [#]((TOP-REAL 2)|P`)by A1,A2,Th38;
  hence thesis;
end;

theorem Th40:
  for s1,s2,t1,t2,P,P2 st s1<s2 & t1<t2 &
  P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
  p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
  P2 = {pb where pb is Point of TOP-REAL 2:
  not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
  P2 c= [#]((TOP-REAL 2)|P`)
proof
  let s1,s2,t1,t2,P,P2;
  assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
  >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
  or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
  t1<=pb`2 & pb`2<=t2)};
  let x be set;
  assume
A5: x in P2;
  then
A6: ex pa being Point of TOP-REAL 2 st pa=x &
  not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A4;
  now
    assume x in { p where p is Point of TOP-REAL 2:
    p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
    p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
    then ex p being Point of TOP-REAL 2 st p=x & (
    p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
    p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1);
    hence contradiction by A1,A2,A6;
  end;
  then x in P` by A3,A5,SUBSET_1:29;
  hence thesis by PRE_TOPC:def 5;
end;

theorem
  for s1,s2,t1,t2,P,P2 st s1<s2 & t1< t2 &
  P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
  p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
  P2 = {pb where pb is Point of TOP-REAL 2:
  not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
  P2 is Subset of (TOP-REAL 2)|P`
proof
  let s1,s2,t1,t2,P,P2;
  assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
  >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
  or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
  t1<=pb`2 & pb`2<=t2)};
  P2 c= [#]((TOP-REAL 2)|P`) by A1,A2,A3,A4,Th40;
  hence thesis;
end;

begin

::
:: The Jordan's property
::

definition
  let S be Subset of TOP-REAL 2;
  attr S is Jordan means
  :Def2:
  S`<> {} & ex A1,A2 being Subset of TOP-REAL 2 st
  S` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 &
  for C1,C2 being Subset of (TOP-REAL 2)|S` st C1 = A1 & C2 = A2 holds
  C1 is a_component & C2 is a_component;
end;

theorem
  for S being Subset of TOP-REAL 2 st S is Jordan holds S`<> {} &
  ex A1,A2 being Subset of TOP-REAL 2 st
  ex C1,C2 being Subset of (TOP-REAL 2)|S` st S` = A1 \/ A2 & A1 misses A2 &
  (Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 &
  C1 is a_component & C2 is a_component &
  for C3 being Subset of (TOP-REAL 2)|S` st C3 is a_component holds
  C3 = C1 or C3 = C2
proof
  let S be Subset of TOP-REAL 2;
  assume
A1: S is Jordan;
  then reconsider S9 = S` as non empty Subset of TOP-REAL 2 by Def2;
  consider A1,A2 being Subset of TOP-REAL 2 such that
A2: S`=A1 \/ A2 and
A3: A1 misses A2 and
A4: (Cl A1)\A1=(Cl A2)\A2 and
A5: for C1,C2 being Subset of (TOP-REAL 2)|S`
  st C1=A1 & C2=A2 holds C1 is a_component & C2 is a_component by A1,Def2;
A6: A1 c= S` by A2,XBOOLE_1:7;
A7: A2 c= S` by A2,XBOOLE_1:7;
A8: [#]((TOP-REAL 2)|S`)=S` by PRE_TOPC:def 5;
  A1 c= [#]((TOP-REAL 2)|S`) by A6,PRE_TOPC:def 5;
  then reconsider G0A=A1,G0B=A2 as Subset of (TOP-REAL 2)|S9 by A7,
PRE_TOPC:def 5;
A9: G0A=A1;
  G0B=A2;
  then
A10: G0A is a_component by A5;
A11: G0B is a_component by A5,A9;
  now
    let C3 be Subset of (TOP-REAL 2)|S9;
    assume
A12: C3 is a_component;
    then
A13: C3 <>{}((TOP-REAL 2)|S9) by CONNSP_1:32;
    C3 /\(G0A \/ G0B)=C3 by A2,A8,XBOOLE_1:28;
    then
A14: (C3 /\ G0A) \/ (C3 /\ G0B) <>{} by A13,XBOOLE_1:23;
    now per cases by A14;
      suppose C3 /\ G0A<>{};
        then
A15:    C3 meets G0A by XBOOLE_0:def 7;
A16:    C3 is connected by A12,CONNSP_1:def 5;
A17:    G0A is connected by A10,CONNSP_1:def 5;
        then
A18:    C3 \/ G0A is connected by A15,A16,CONNSP_1:1,17;
        G0A c= C3 \/ G0A by XBOOLE_1:7;
        then G0A=C3 \/ G0A by A10,A18,CONNSP_1:def 5;
        then C3 c= G0A by XBOOLE_1:7;
        hence C3=G0A or C3=G0B by A12,A17,CONNSP_1:def 5;
      end;
      suppose C3 /\ A2<>{};
        then
A19:    C3 meets G0B by XBOOLE_0:def 7;
A20:    C3 is connected by A12,CONNSP_1:def 5;
A21:    G0B is connected by A11,CONNSP_1:def 5;
        then
A22:    C3 \/ G0B is connected by A19,A20,CONNSP_1:1,17;
        G0B c= C3 \/ G0B by XBOOLE_1:7;
        then G0B=C3 \/ G0B by A11,A22,CONNSP_1:def 5;
        then C3 c= G0B by XBOOLE_1:7;
        hence C3=G0A or C3=G0B by A12,A21,CONNSP_1:def 5;
      end;
    end;
    hence C3=G0A or C3=G0B;
  end;
  hence thesis by A2,A3,A4,A10,A11;
end;

theorem
  for s1,s2,t1,t2 for P being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
  P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
  p`1 = s2 & p`2 <= t2 & p`2 >= t1} holds P is Jordan
proof
  let s1,s2,t1,t2;
  let P be Subset of TOP-REAL 2;
  assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2:
  p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
  reconsider P1= {pa where pa is Point of TOP-REAL 2:
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2},
  P2= {pc where pc is Point of TOP-REAL 2:
  not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2)}
  as Subset of TOP-REAL 2 by Th29,Th30;
  reconsider PC = P` as Subset of TOP-REAL 2;
A4: P1= {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa`2 &
  pa`2 < t2};
A5: P2= {pc where pc is Point of TOP-REAL 2: not( s1<=pc`1 & pc`1<=s2 & t1<=
  pc`2 & pc`2<=t2)};
A6: PC=P1 \/ P2 by A1,A2,A3,Th36;
A7: PC<>{} by A1,A2,A3,A4,A5,Th36;
A8: P1 misses P2 by A1,A2,A3,Th36;
A9: P=(Cl P1)\P1 by A1,A2,A3,A5,Th37;
A10: P=(Cl P2)\P2 by A1,A2,A3,A4,Th37;
  for P1A,P2B be Subset of (TOP-REAL 2)|P` holds P1A=P1 & P2B=P2 implies
  P1A is a_component & P2B is a_component by A1,A2,A3,Th36;
  hence thesis by A6,A7,A8,A9,A10,Def2;
end;

theorem
  for s1,t1,s2,t2 for P,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
  P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
  p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
  P2 = {pb where pb is Point of TOP-REAL 2:
  not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)}
  holds Cl P2 = P \/ P2 by Lm11;

theorem
  for s1,t1,s2,t2 for P,P1 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
  P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
  p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
  p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
  P1 = {pa where pa is Point of TOP-REAL 2:
  s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds Cl P1 = P \/ P1 by Lm10;

:: Moved from JORDAN1H, AK, 22.02.2006

theorem
  for p,q being Point of TOP-REAL 2 holds LSeg(p,q) \ {p,q} is convex
proof
  let p,q,w1,w2 be Point of TOP-REAL 2;
  set P = LSeg(p,q) \ {p,q};
  assume that
A1: w1 in P and
A2: w2 in P;
A3: w1 in LSeg(p,q) by A1,XBOOLE_0:def 5;
A4: w2 in LSeg(p,q) by A2,XBOOLE_0:def 5;
A5: not w1 in {p,q} by A1,XBOOLE_0:def 5;
A6: not w2 in {p,q} by A2,XBOOLE_0:def 5;
A7: w1 <> p by A5,TARSKI:def 2;
A8: w2 <> p by A6,TARSKI:def 2;
A9: w1 <> q by A5,TARSKI:def 2;
A10: w2 <> q by A6,TARSKI:def 2;
A11: not p in LSeg(w1,w2) by A3,A4,A7,A8,SPPOL_1:7,TOPREAL1:6;
  not q in LSeg(w1,w2) by A3,A4,A9,A10,SPPOL_1:7,TOPREAL1:6;
  then LSeg(w1,w2) misses {p,q} by A11,ZFMISC_1:51;
  hence thesis by A3,A4,TOPREAL1:6,XBOOLE_1:86;
end;

:: Moved from JORDAN1A, AK, 22.02.2006

Lm12: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x,y0 ]| where x is Real : x <= x0 } holds P is convex
proof
  let x0,y0 be Real;
  let P be Subset of TOP-REAL 2;
  assume
A1: P = {|[ x,y0 ]| where x is Real : x <= x0 };
  let w1,w2 be Point of TOP-REAL 2;
  assume that
A2: w1 in P and
A3: w2 in P;
  consider x1 being Real such that
A4: w1 = |[ x1,y0 ]| and
A5: x1 <= x0 by A1,A2;
  consider x2 being Real such that
A6: w2 = |[ x2,y0 ]| and
A7: x2 <= x0 by A1,A3;
  let v be set;
  assume
A8: v in LSeg(w1,w2);
  then reconsider v1 = v as Point of TOP-REAL 2;
  consider l being Real such that
A9: v1 = (1-l)*w1 + l*w2 and
A10: 0 <= l and
A11: l <= 1 by A8;
A12: v1 = |[ (1-l)*x1,(1-l)*y0 ]| + l*|[ x2,y0 ]| by A4,A6,A9,EUCLID:58
    .= |[ (1-l)*x1,(1-l)*y0 ]| + |[ l*x2,l*y0 ]| by EUCLID:58
    .= |[ (1-l)*x1+l*x2,(1-l)*y0+l*y0 ]| by EUCLID:56
    .= |[ (1-l)*x1+l*x2,1 * y0 ]|;
  (1-l)*x1+l*x2 <= x0 by A5,A7,A10,A11,XREAL_1:174;
  hence thesis by A1,A12;
end;

Lm13: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x0,y ]| where y is Real : y <= y0 } holds P is convex
proof
  let x0,y0 be Real;
  let P be Subset of TOP-REAL 2;
  assume
A1: P = {|[ x0,y ]| where y is Real : y <= y0 };
  let w1,w2 be Point of TOP-REAL 2;
  assume that
A2: w1 in P and
A3: w2 in P;
  consider y1 being Real such that
A4: w1 = |[ x0,y1 ]| and
A5: y1 <= y0 by A1,A2;
  consider y2 being Real such that
A6: w2 = |[ x0,y2 ]| and
A7: y2 <= y0 by A1,A3;
  let v be set;
  assume
A8: v in LSeg(w1,w2);
  then reconsider v1 = v as Point of TOP-REAL 2;
  consider l being Real such that
A9: v1 = (1-l)*w1 + l*w2 and
A10: 0 <= l and
A11: l <= 1 by A8;
A12: v1 = |[ (1-l)*x0,(1-l)*y1 ]| + l*|[ x0,y2 ]| by A4,A6,A9,EUCLID:58
    .= |[ (1-l)*x0,(1-l)*y1 ]| + |[ l*x0,l*y2 ]| by EUCLID:58
    .= |[ (1-l)*x0+l*x0,(1-l)*y1+l*y2 ]| by EUCLID:56
    .= |[ 1 * x0,(1-l)*y1+l*y2 ]|;
  (1-l)*y1+l*y2 <= y0 by A5,A7,A10,A11,XREAL_1:174;
  hence thesis by A1,A12;
end;

Lm14: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x,y0 ]| where x is Real : x >= x0 } holds P is convex
proof
  let x0,y0 be Real;
  let P be Subset of TOP-REAL 2;
  assume
A1: P = {|[ x,y0 ]| where x is Real : x >= x0 };
  let w1,w2 be Point of TOP-REAL 2;
  assume that
A2: w1 in P and
A3: w2 in P;
  consider x1 being Real such that
A4: w1 = |[ x1,y0 ]| and
A5: x1 >= x0 by A1,A2;
  consider x2 being Real such that
A6: w2 = |[ x2,y0 ]| and
A7: x2 >= x0 by A1,A3;
  let v be set;
  assume
A8: v in LSeg(w1,w2);
  then reconsider v1 = v as Point of TOP-REAL 2;
  v1 in { (1-l)*w2 + l*w1 where l is Real : 0 <= l & l <= 1 }
  by A8,RLTOPSP1:def 2;
  then consider l being Real such that
A9: v1 = (1-l)*w2 + l*w1 and
A10: 0 <= l and
A11: l <= 1;
A12: v1 = |[ (1-l)*x2,(1-l)*y0 ]| + l*|[ x1,y0 ]| by A4,A6,A9,EUCLID:58
    .= |[ (1-l)*x2,(1-l)*y0 ]| + |[ l*x1,l*y0 ]| by EUCLID:58
    .= |[ (1-l)*x2+l*x1,(1-l)*y0+l*y0 ]| by EUCLID:56
    .= |[ (1-l)*x2+l*x1,1 * y0 ]|;
  (1-l)*x2+l*x1 >= x0 by A5,A7,A10,A11,XREAL_1:173;
  hence thesis by A1,A12;
end;

Lm15: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x0,y ]| where y is Real : y >= y0 } holds P is convex
proof
  let x0,y0 be Real;
  let P be Subset of TOP-REAL 2;
  assume
A1: P = {|[ x0,y ]| where y is Real : y >= y0 };
  let w1,w2 be Point of TOP-REAL 2;
  assume that
A2: w1 in P and
A3: w2 in P;
  consider x1 being Real such that
A4: w1 = |[ x0,x1 ]| and
A5: x1 >= y0 by A1,A2;
  consider x2 being Real such that
A6: w2 = |[ x0,x2 ]| and
A7: x2 >= y0 by A1,A3;
  let v be set;
  assume
A8: v in LSeg(w1,w2);
  then reconsider v1 = v as Point of TOP-REAL 2;
  v1 in { (1-l)*w2 + l*w1 where l is Real : 0 <= l & l <= 1 }
  by A8,RLTOPSP1:def 2;
  then consider l being Real such that
A9: v1 = (1-l)*w2 + l*w1 and
A10: 0 <= l and
A11: l <= 1;
A12: v1 = |[ (1-l)*x0,(1-l)*x2 ]| + l*|[ x0,x1 ]| by A4,A6,A9,EUCLID:58
    .= |[ (1-l)*x0,(1-l)*x2 ]| + |[ l*x0,l*x1 ]| by EUCLID:58
    .= |[ (1-l)*x0+l*x0,(1-l)*x2+l*x1 ]| by EUCLID:56
    .= |[ 1 * x0,(1-l)*x2+l*x1]|;
  (1-l)*x2+l*x1 >= y0 by A5,A7,A10,A11,XREAL_1:173;
  hence thesis by A1,A12;
end;

registration
  let p be Point of TOP-REAL 2;
  cluster north_halfline p -> convex;
  coherence
  proof
    north_halfline p =
    { |[ p`1,r ]| where r is Element of REAL: r >= p`2 } by TOPREAL1:31;
    hence thesis by Lm15;
  end;
  cluster east_halfline p -> convex;
  coherence
  proof
    east_halfline p =
    { |[ r,p`2 ]| where r is Element of REAL: r >= p`1 } by TOPREAL1:33;
    hence thesis by Lm14;
  end;
  cluster south_halfline p -> convex;
  coherence
  proof
    south_halfline p =
    { |[ p`1,r ]| where r is Element of REAL: r <= p`2 } by TOPREAL1:35;
    hence thesis by Lm13;
  end;
  cluster west_halfline p -> convex;
  coherence
  proof
    west_halfline p =
    { |[ r,p`2 ]| where r is Element of REAL: r <= p`1 } by TOPREAL1:37;
    hence thesis by Lm12;
  end;
end;