jordan1.miz



    begin

    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 :: JORDAN1:1

    

     Th1: for GX be non empty TopSpace st (for x,y be Point of GX holds ex h be 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 be Point of GX holds ex h be Function of I[01] , GX st h is continuous & x = (h . 0 ) & y = (h . 1);

      for x,y be Point of GX holds ex GY st (GY is connected & ex f be Function of GY, GX st f is continuous & x in ( rng f) & y in ( rng f))

      proof

        let x, y;

        now

          consider h be 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 :: JORDAN1:2

    

     Th2: for A be Subset of GX st (for xa,ya be Point of GX st xa in A & ya in A & xa <> ya holds ex h be 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 be Point of GX st xa in A & ya in A & xa <> ya holds ex h be 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 be Point of GX st xa in A & ya in A & xa = ya holds ex h be 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 be Point of (GX | A) holds ex ha be 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;

      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 :: JORDAN1:3

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

    theorem :: JORDAN1:4

    

     Th4: for A0,A1,A2 be 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;

      

       A7: (A0 \/ A1) is connected by A1, A2, A4, CONNSP_1: 1, CONNSP_1: 17;

      ((A0 \/ A1) /\ A2) = ((A0 /\ A2) \/ (A1 /\ A2)) by XBOOLE_1: 23;

      then (A0 \/ A1) meets A2 by A6;

      hence thesis by A3, A7, CONNSP_1: 1, CONNSP_1: 17;

    end;

    theorem :: JORDAN1:5

    

     Th5: for A0,A1,A2,A3 be 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;

      

       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;

      hence thesis by A4, A9, CONNSP_1: 1, CONNSP_1: 17;

    end;

    begin

    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;

      :: original: convex

      redefine

      :: JORDAN1:def1

      attr P is convex means for w1,w2 be 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 be Point of ( TOP-REAL n) st w3 in P & w4 in P holds ( LSeg (w3,w4)) c= P;

        for w1,w2 be Point of ( TOP-REAL n) st w1 in P & w2 in P & w1 <> w2 holds ex h be 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 be 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 object;

        assume y in { |[sb, tb]| : sb < s1 };

        then

        consider s7,t7 be 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 object;

        assume y in { |[sd, td]| : td < t1 };

        then

        consider s7,t7 be 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 object;

        assume y in { |[sb, tb]| : s2 < sb };

        then

        consider s7,t7 be 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 object;

        assume y in { |[sb, tb]| : t2 < tb };

        then

        consider s7,t7 be 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 be Real, t be Real : s1 < s & s < s2 & t1 < t & t < t2 } is Subset of ( REAL 2)

    proof

      let s1, s2, t1, t2;

      { |[sb, tb]| where sb be Real, tb be Real : s1 < sb & sb < s2 & t1 < tb & tb < t2 } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[sb, tb]| where sb be Real, tb be Real : s1 < sb & sb < s2 & t1 < tb & tb < t2 };

        then

        consider s7,t7 be 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 be Real, tb be Real : not (s1 <= sb & sb <= s2 & t1 <= tb & tb <= t2) } c= ( REAL 2)

      proof

        let y be object;

        assume y in { |[sb, tb]| where sb be Real, tb be Real : not (s1 <= sb & sb <= s2 & t1 <= tb & tb <= t2) };

        then

        consider s7,t7 be 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 :: JORDAN1:7

    

     Th6: { |[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 object;

        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 });

      now

        let x be object;

        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 };

      hence thesis by A6;

    end;

    theorem :: JORDAN1:8

    

     Th7: { |[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 object;

        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 });

      now

        let x be object;

        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) };

      hence thesis by A1;

    end;

    theorem :: JORDAN1:9

    

     Th8: 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 object 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 :: JORDAN1:11

    

     Th9: 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 object 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 :: JORDAN1:13

    

     Th10: 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 object 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 :: JORDAN1:15

    

     Th11: 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 object 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 :: JORDAN1:17

    

     Th12: 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 object 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 :: JORDAN1:19

    

     Th13: 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 Th7;

      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;

      

       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;

      

       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;

      

       A12: A0 is convex by Th10;

      

       A13: A1 is convex by Th12;

      

       A14: A2 is convex by Th9;

      A3 is convex by Th11;

      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 :: JORDAN1:20

    

     Th14: for s1 holds { |[s, t]| : s1 < s } is open Subset of ( TOP-REAL 2)

    proof

      let s1;

      reconsider P = { |[s, t]| : s1 < s } as Subset of ( REAL 2) by Lm5;

      reconsider PP = P as Subset of ( TopSpaceMetr ( Euclid 2));

      for pe be Point of ( Euclid 2) st pe in P holds ex r be Real 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

         A1: |[s, t]| = pe and

         A2: s1 < s;

        set r = ((s - s1) / 2);

        

         A3: (s - s1) > 0 by A2, XREAL_1: 50;

        then

         A4: r > 0 by XREAL_1: 139;

        ( Ball (pe,r)) c= P

        proof

          let x be object;

          assume x in ( Ball (pe,r));

          then x in { q where q be Element of ( Euclid 2) : ( dist (pe,q)) < r } by METRIC_1: 17;

          then

          consider q be Element of ( Euclid 2) such that

           A5: q = x and

           A6: ( 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

           A7: ( sqrt ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ))) < r by A6, TOPREAL3: 7;

          

           A8: 0 <= (((ppe `1 ) - (pq `1 )) ^2 ) by XREAL_1: 63;

           0 <= (((ppe `2 ) - (pq `2 )) ^2 ) by XREAL_1: 63;

          then

           A9: ( 0 + 0 ) <= ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) by A8, 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 A7, SQUARE_1: 16;

          then

           A10: ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) < (r ^2 ) by A9, SQUARE_1:def 2;

          (((ppe `1 ) - (pq `1 )) ^2 ) <= ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) by XREAL_1: 31, XREAL_1: 63;

          then (((ppe `1 ) - (pq `1 )) ^2 ) < (r ^2 ) by A10, XXREAL_0: 2;

          then ((ppe `1 ) - (pq `1 )) < r by A4, SQUARE_1: 15;

          then (ppe `1 ) < ((pq `1 ) + r) by XREAL_1: 19;

          then ((ppe `1 ) - r) < (pq `1 ) by XREAL_1: 19;

          then

           A11: (s - ((s - s1) / 2)) < (pq `1 ) by A1, EUCLID: 52;

          (s - ((s - s1) / 2)) = (r + s1);

          then

           A12: s1 < (s - ((s - s1) / 2)) by A3, XREAL_1: 29, XREAL_1: 139;

          

           A13: |[(pq `1 ), (pq `2 )]| = x by A5, EUCLID: 53;

          s1 < (pq `1 ) by A11, A12, XXREAL_0: 2;

          hence thesis by A13;

        end;

        hence thesis by A3, XREAL_1: 139;

      end;

      then PP is open by TOPMETR: 15;

      hence thesis by Lm9, PRE_TOPC: 30;

    end;

    theorem :: JORDAN1:21

    

     Th15: for s1 holds { |[s, t]| : s1 > s } is open Subset of ( TOP-REAL 2)

    proof

      let s1;

      reconsider P = { |[s, t]| : s1 > s } as Subset of ( REAL 2) by Lm3;

      reconsider PP = P as Subset of ( TopSpaceMetr ( Euclid 2));

      for pe be Point of ( Euclid 2) st pe in P holds ex r be Real 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

         A1: |[s, t]| = pe and

         A2: s1 > s;

        set r = ((s1 - s) / 2);

        

         A3: (s1 - s) > 0 by A2, XREAL_1: 50;

        then

         A4: r > 0 by XREAL_1: 139;

        ( Ball (pe,r)) c= P

        proof

          let x be object;

          assume x in ( Ball (pe,r));

          then x in { q where q be Element of ( Euclid 2) : ( dist (pe,q)) < r } by METRIC_1: 17;

          then

          consider q be Element of ( Euclid 2) such that

           A5: q = x and

           A6: ( 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

           A7: ( sqrt ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ))) < r by A6, TOPREAL3: 7;

          

           A8: 0 <= (((ppe `1 ) - (pq `1 )) ^2 ) by XREAL_1: 63;

           0 <= (((ppe `2 ) - (pq `2 )) ^2 ) by XREAL_1: 63;

          then

           A9: ( 0 + 0 ) <= ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) by A8, 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 A7, SQUARE_1: 16;

          then

           A10: ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) < (r ^2 ) by A9, SQUARE_1:def 2;

          (((ppe `1 ) - (pq `1 )) ^2 ) <= ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) by XREAL_1: 31, XREAL_1: 63;

          then (((pq `1 ) - (ppe `1 )) ^2 ) < (r ^2 ) by A10, XXREAL_0: 2;

          then ((pq `1 ) - (ppe `1 )) < r by A4, SQUARE_1: 15;

          then ((ppe `1 ) + r) > (pq `1 ) by XREAL_1: 19;

          then

           A11: (s + ((s1 - s) / 2)) > (pq `1 ) by A1, EUCLID: 52;

          (s + ((s1 - s) / 2)) = (s1 - r);

          then

           A12: s1 > (s + ((s1 - s) / 2)) by A3, XREAL_1: 44, XREAL_1: 139;

          

           A13: |[(pq `1 ), (pq `2 )]| = x by A5, EUCLID: 53;

          s1 > (pq `1 ) by A11, A12, XXREAL_0: 2;

          hence thesis by A13;

        end;

        hence thesis by A3, XREAL_1: 139;

      end;

      then PP is open by TOPMETR: 15;

      hence thesis by Lm9, PRE_TOPC: 30;

    end;

    theorem :: JORDAN1:22

    

     Th16: for s1 holds { |[s, t]| : s1 < t } is open Subset of ( TOP-REAL 2)

    proof

      let s1;

      reconsider P = { |[s, t]| : s1 < t } as Subset of ( REAL 2) by Lm6;

      reconsider PP = P as Subset of ( TopSpaceMetr ( Euclid 2));

      for pe be Point of ( Euclid 2) st pe in P holds ex r be Real 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

         A1: |[s, t]| = pe and

         A2: s1 < t;

        set r = ((t - s1) / 2);

        

         A3: (t - s1) > 0 by A2, XREAL_1: 50;

        then

         A4: r > 0 by XREAL_1: 139;

        ( Ball (pe,r)) c= P

        proof

          let x be object;

          assume x in ( Ball (pe,r));

          then x in { q where q be Element of ( Euclid 2) : ( dist (pe,q)) < r } by METRIC_1: 17;

          then

          consider q be Element of ( Euclid 2) such that

           A5: q = x and

           A6: ( 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

           A7: ( sqrt ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ))) < r by A6, TOPREAL3: 7;

          

           A8: 0 <= (((ppe `1 ) - (pq `1 )) ^2 ) by XREAL_1: 63;

           0 <= (((ppe `2 ) - (pq `2 )) ^2 ) by XREAL_1: 63;

          then

           A9: ( 0 + 0 ) <= ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) by A8, 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 A7, SQUARE_1: 16;

          then

           A10: ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) < (r ^2 ) by A9, SQUARE_1:def 2;

          (((ppe `2 ) - (pq `2 )) ^2 ) <= ((((ppe `2 ) - (pq `2 )) ^2 ) + (((ppe `1 ) - (pq `1 )) ^2 )) by XREAL_1: 31, XREAL_1: 63;

          then (((ppe `2 ) - (pq `2 )) ^2 ) < (r ^2 ) by A10, XXREAL_0: 2;

          then ((ppe `2 ) - (pq `2 )) < r by A4, SQUARE_1: 15;

          then (ppe `2 ) < ((pq `2 ) + r) by XREAL_1: 19;

          then ((ppe `2 ) - r) < (pq `2 ) by XREAL_1: 19;

          then

           A11: (t - ((t - s1) / 2)) < (pq `2 ) by A1, EUCLID: 52;

          (t - ((t - s1) / 2)) = (r + s1);

          then

           A12: s1 < (t - ((t - s1) / 2)) by A3, XREAL_1: 29, XREAL_1: 139;

          

           A13: |[(pq `1 ), (pq `2 )]| = x by A5, EUCLID: 53;

          s1 < (pq `2 ) by A11, A12, XXREAL_0: 2;

          hence thesis by A13;

        end;

        hence thesis by A3, XREAL_1: 139;

      end;

      then PP is open by TOPMETR: 15;

      hence thesis by Lm9, PRE_TOPC: 30;

    end;

    theorem :: JORDAN1:23

    

     Th17: for s1 holds { |[s, t]| : s1 > t } is open Subset of ( TOP-REAL 2)

    proof

      let s1;

      reconsider P = { |[s, t]| : s1 > t } as Subset of ( REAL 2) by Lm4;

      reconsider PP = P as Subset of ( TopSpaceMetr ( Euclid 2));

      for pe be Point of ( Euclid 2) st pe in P holds ex r be Real 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

         A1: |[s, t]| = pe and

         A2: s1 > t;

        set r = ((s1 - t) / 2);

        

         A3: (s1 - t) > 0 by A2, XREAL_1: 50;

        then

         A4: r > 0 by XREAL_1: 139;

        ( Ball (pe,r)) c= P

        proof

          let x be object;

          assume x in ( Ball (pe,r));

          then x in { q where q be Element of ( Euclid 2) : ( dist (pe,q)) < r } by METRIC_1: 17;

          then

          consider q be Element of ( Euclid 2) such that

           A5: q = x and

           A6: ( 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

           A7: ( sqrt ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 ))) < r by A6, TOPREAL3: 7;

          

           A8: 0 <= (((ppe `1 ) - (pq `1 )) ^2 ) by XREAL_1: 63;

           0 <= (((ppe `2 ) - (pq `2 )) ^2 ) by XREAL_1: 63;

          then

           A9: ( 0 + 0 ) <= ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) by A8, 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 A7, SQUARE_1: 16;

          then

           A10: ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) < (r ^2 ) by A9, SQUARE_1:def 2;

          (((ppe `2 ) - (pq `2 )) ^2 ) <= ((((ppe `1 ) - (pq `1 )) ^2 ) + (((ppe `2 ) - (pq `2 )) ^2 )) by XREAL_1: 31, XREAL_1: 63;

          then (((pq `2 ) - (ppe `2 )) ^2 ) < (r ^2 ) by A10, XXREAL_0: 2;

          then ((pq `2 ) - (ppe `2 )) < r by A4, SQUARE_1: 15;

          then ((ppe `2 ) + r) > (pq `2 ) by XREAL_1: 19;

          then

           A11: (t + ((s1 - t) / 2)) > (pq `2 ) by A1, EUCLID: 52;

          (t + ((s1 - t) / 2)) = (s1 - r);

          then

           A12: s1 > (t + ((s1 - t) / 2)) by A3, XREAL_1: 44, XREAL_1: 139;

          

           A13: |[(pq `1 ), (pq `2 )]| = x by A5, EUCLID: 53;

          s1 > (pq `2 ) by A11, A12, XXREAL_0: 2;

          hence thesis by A13;

        end;

        hence thesis by A3, XREAL_1: 139;

      end;

      then PP is open by TOPMETR: 15;

      hence thesis by Lm9, PRE_TOPC: 30;

    end;

    theorem :: JORDAN1:24

    

     Th18: for s1, t1, s2, t2 holds { |[s, t]| : s1 < s & s < s2 & t1 < t & t < t2 } is open Subset of ( TOP-REAL 2)

    proof

      let s1, t1, s2, t2;

      set 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;

      

       A1: P = (((P1 /\ P2) /\ P3) /\ P4) by Th6;

      

       A2: P1 is open by Th14;

      P2 is open by Th15;

      then

       A3: (P1 /\ P2) is open by A2, TOPS_1: 11;

      

       A4: P3 is open by Th16;

      

       A5: P4 is open by Th17;

      ((P1 /\ P2) /\ P3) is open by A3, A4, TOPS_1: 11;

      hence thesis by A1, A5, TOPS_1: 11;

    end;

    theorem :: JORDAN1:25

    

     Th19: for s1, t1, s2, t2 holds { |[s, t]| : not (s1 <= s & s <= s2 & t1 <= t & t <= t2) } is open Subset of ( TOP-REAL 2)

    proof

      let s1, t1, s2, t2;

      set P = { |[s, t]| : not (s1 <= s & s <= s2 & t1 <= t & t <= t2) };

      

       A1: P = ((({ |[s3, t3]| : s3 < s1 } \/ { |[s4, t4]| : t4 < t1 }) \/ { |[s5, t5]| : s2 < s5 }) \/ { |[s6, t6]| : t2 < t6 }) by Th7;

      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 Th15;

      A1 is open by Th17;

      then

       A3: (A0 \/ A1) is open by A2, TOPS_1: 10;

      A2 is open by Th14;

      then

       A4: ((A0 \/ A1) \/ A2) is open by A3, TOPS_1: 10;

      A3 is open by Th16;

      hence thesis by A1, A4, TOPS_1: 10;

    end;

    theorem :: JORDAN1:26

    

     Th20: 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 object 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 :: JORDAN1:27

    

     Th21: for s1,s2,t1,t2 be Real holds { p where p be 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 object;

         A1:

        now

          assume x in { p where p be Point of ( TOP-REAL 2) : s1 < (p `1 ) & (p `1 ) < s2 & t1 < (p `2 ) & (p `2 ) < t2 };

          then

          consider pp be 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 be 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 be 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 be 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: 2;

    end;

    theorem :: JORDAN1:28

    

     Th22: for s1, s2, t1, t2 holds { qc where qc be 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 object;

         A1:

        now

          assume x in { qc where qc be Point of ( TOP-REAL 2) : not (s1 <= (qc `1 ) & (qc `1 ) <= s2 & t1 <= (qc `2 ) & (qc `2 ) <= t2) };

          then

          consider q be 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 be 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 be 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 be 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: 2;

    end;

    theorem :: JORDAN1:29

    

     Th23: for s1, s2, t1, t2 holds { p0 where p0 be 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 Th21;

    end;

    theorem :: JORDAN1:30

    

     Th24: for s1, s2, t1, t2 holds { pq where pq be 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 Th22;

    end;

    theorem :: JORDAN1:31

    

     Th25: for s1, t1, s2, t2, P st P = { p0 where p0 be 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 be 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 Th21;

      hence thesis by Th8;

    end;

    theorem :: JORDAN1:32

    

     Th26: for s1, t1, s2, t2, P st P = { pq where pq be 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 be 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 Th22;

      hence thesis by Th13;

    end;

    theorem :: JORDAN1:33

    

     Th27: for s1, t1, s2, t2 holds for P be Subset of ( TOP-REAL 2) st P = { p0 where p0 be 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 be 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 Th21;

      hence thesis by Th18;

    end;

    theorem :: JORDAN1:34

    

     Th28: for s1, t1, s2, t2 holds for P be Subset of ( TOP-REAL 2) st P = { pq where pq be 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 be 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 Th22;

      hence thesis by Th19;

    end;

    theorem :: JORDAN1:35

    

     Th29: for s1, t1, s2, t2, P, Q st P = { p where p be Point of ( TOP-REAL 2) : s1 < (p `1 ) & (p `1 ) < s2 & t1 < (p `2 ) & (p `2 ) < t2 } & Q = { qc where qc be 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 be Point of ( TOP-REAL 2) : s1 < (p `1 ) & (p `1 ) < s2 & t1 < (p `2 ) & (p `2 ) < t2 } and

       A2: Q = { qc where qc be 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, Th21;

      Q = { |[sb, tb]| : not (s1 <= sb & sb <= s2 & t1 <= tb & tb <= t2) } by A2, Th22;

      hence thesis by A3, Th20;

    end;

    theorem :: JORDAN1:36

    

     Th30: for s1, t1, s2, t2 holds for P,P1,P2 be Subset of ( TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 } & P2 = { pb where pb be 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 be 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 be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 } and

       A5: P2 = { pc where pc be Point of ( TOP-REAL 2) : not (s1 <= (pc `1 ) & (pc `1 ) <= s2 & t1 <= (pc `2 ) & (pc `2 ) <= t2) };

      now

        let x be object;

        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);

      now

        let x be object 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 be 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 be 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 ` );

      hence

       A15: (P ` ) = (P1 \/ P2) by A8;

      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 be 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, Th29;

      hence

       A26: (P1 /\ P2) = {} ;

      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, Th25;

        then

         A29: P1A is connected by A27, CONNSP_1: 23;

        

         A30: P2 is connected by A5, Th26;

        

         A31: P2 = { |[sa, ta]| : not (s1 <= sa & sa <= s2 & t1 <= ta & ta <= t2) } by A5, Th22;

        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, Th7;

        (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 be 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;

          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, Th27;

            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, Th28;

            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, Th29;

              then (P1 /\ P2) = {} ;

              then AP misses BP by A27, A28, A51;

              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;

        for CP be 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;

          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, Th28;

          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, Th27;

          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;

            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;

      end;

      hence thesis;

    end;

    

     Lm10: for s1, t1, s2, t2 holds for P,P1 be Subset of ( TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p be 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 be 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 be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 };

      reconsider P2 = { pb where pb be 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 Th24;

      

       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, Th30;

      P1 misses P2 by A1, A2, A3, A4, Th30;

      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 object;

        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);

      now

        let x be object;

        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 ` );

      then

       A12: (P2 ` ) = (P \/ P1) by A11;

      

       A13: P2 is open by Th28;

      (( [#] ( 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) by A14, A15, PRE_TOPC: 15;

      P c= ( Cl P1)

      proof

        let x be object;

        assume x in P;

        then

        consider p be 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 be 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 such that

                   A22: r > 0 and

                   A23: ( Ball (q,r)) c= Q by A21, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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 be 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 such that

                   A45: r > 0 and

                   A46: ( Ball (q,r)) c= Q by A44, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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, XREAL_1: 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 be 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 such that

                   A70: r > 0 and

                   A71: ( Ball (q,r)) c= Q by A69, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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, XREAL_1: 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 be 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 such that

                   A96: r > 0 and

                   A97: ( Ball (q,r)) c= Q by A95, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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 be 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 such that

                   A118: r > 0 and

                   A119: ( Ball (q,r)) c= Q by A117, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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, XREAL_1: 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 be 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 such that

                   A143: r > 0 and

                   A144: ( Ball (q,r)) c= Q by A142, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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, XREAL_1: 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 be 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 such that

                   A169: r > 0 and

                   A170: ( Ball (q,r)) c= Q by A168, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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 be 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 such that

                   A192: r > 0 and

                   A193: ( Ball (q,r)) c= Q by A191, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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, XREAL_1: 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 be 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 such that

                   A217: r > 0 and

                   A218: ( Ball (q,r)) c= Q by A216, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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, XREAL_1: 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 be 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 be Real such that

                   A243: r > 0 and

                   A244: ( Ball (q,r)) c= Q by A242, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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 be 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 be Real such that

                   A265: r > 0 and

                   A266: ( Ball (q,r)) c= Q by A264, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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, XREAL_1: 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 be 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 be Real such that

                   A290: r > 0 and

                   A291: ( Ball (q,r)) c= Q by A289, TOPMETR: 15;

                  reconsider r as Real;

                  

                   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, XREAL_1: 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 holds for P,P2 be Subset of ( TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p be 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 be 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 be 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 be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 } as Subset of ( TOP-REAL 2) by Th23;

      reconsider PP = (P ` ) as Subset of ( TOP-REAL 2);

      

       A6: PP = (P1 \/ P2) by A1, A2, A3, A4, Th30;

      P1 misses P2 by A1, A2, A3, A4, Th30;

      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 object;

        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);

      now

        let x be object;

        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 ` );

      then

       A12: (P1 ` ) = (P \/ P2) by A11;

      

       A13: P1 is open by Th27;

      (( [#] ( 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) by A14, A15, PRE_TOPC: 15;

      P c= ( Cl P2)

      proof

        let x be object;

        assume x in P;

        then

        consider p be 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 be 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 such that

               A21: r > 0 and

               A22: ( Ball (q,r)) c= Q by A20, TOPMETR: 15;

              reconsider r as Real;

              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, XREAL_1: 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;

            end;

            hence thesis by A16, PRE_TOPC:def 7;

          end;

            suppose

             A30: (p `1 ) <= s2 & (p `1 ) >= s1 & (p `2 ) = t2;

            for Q be 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 be Real such that

               A33: r > 0 and

               A34: ( Ball (q,r)) c= Q by A32, TOPMETR: 15;

              reconsider r as Real;

              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, XREAL_1: 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;

            end;

            hence thesis by A16, PRE_TOPC:def 7;

          end;

            suppose

             A43: (p `1 ) <= s2 & (p `1 ) >= s1 & (p `2 ) = t1;

            for Q be 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 be Real such that

               A46: r > 0 and

               A47: ( Ball (q,r)) c= Q by A45, TOPMETR: 15;

              reconsider r as Real;

              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, XREAL_1: 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 be 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 be Real such that

               A58: r > 0 and

               A59: ( Ball (q,r)) c= Q by A57, TOPMETR: 15;

              reconsider r as Real;

              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, XREAL_1: 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 :: JORDAN1:37

    

     Th31: for s1, t1, s2, t2 holds for P,P1,P2 be Subset of ( TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 } & P2 = { pb where pb be 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 be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 } and

       A5: P2 = { pb where pb be 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, Th30;

      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 object;

        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 object;

        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;

    end;

    theorem :: JORDAN1:38

    

     Th32: for s1, s2, t1, t2, P, P1 st P = { p where p be 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 be 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 be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 };

      let x be object;

      assume

       A3: x in P1;

      then

       A4: ex pa be 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 be 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 be 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 :: JORDAN1:39

    for s1, s2, t1, t2, P, P1 st P = { p where p be 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 be 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 be 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 be 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, Th32;

      hence thesis;

    end;

    theorem :: JORDAN1:40

    

     Th34: for s1, s2, t1, t2, P, P2 st s1 < s2 & t1 < t2 & P = { p where p be 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 be 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 be 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 be Point of ( TOP-REAL 2) : not (s1 <= (pb `1 ) & (pb `1 ) <= s2 & t1 <= (pb `2 ) & (pb `2 ) <= t2) };

      let x be object;

      assume

       A5: x in P2;

      then

       A6: ex pa be 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 be 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 be 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 :: JORDAN1:41

    for s1, s2, t1, t2, P, P2 st s1 < s2 & t1 < t2 & P = { p where p be 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 be 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 be 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 be 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, Th34;

      hence thesis;

    end;

    begin

    definition

      let S be Subset of ( TOP-REAL 2);

      :: JORDAN1:def2

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

    end

    theorem :: JORDAN1:42

    for S be Subset of ( TOP-REAL 2) st S is Jordan holds (S ` ) <> {} & ex A1,A2 be Subset of ( TOP-REAL 2) st ex C1,C2 be 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 be 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);

      consider A1,A2 be 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 be Subset of (( TOP-REAL 2) | (S ` )) st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component by A1;

      

       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;

            

             A16: C3 is connected by A12;

            

             A17: G0A is connected by A10;

            then

             A18: (C3 \/ G0A) is connected by A15, A16, CONNSP_1: 1, CONNSP_1: 17;

            G0A c= (C3 \/ G0A) by XBOOLE_1: 7;

            then G0A = (C3 \/ G0A) by A10, A18;

            then C3 c= G0A by XBOOLE_1: 7;

            hence C3 = G0A or C3 = G0B by A12, A17;

          end;

            suppose (C3 /\ A2) <> {} ;

            then

             A19: C3 meets G0B;

            

             A20: C3 is connected by A12;

            

             A21: G0B is connected by A11;

            then

             A22: (C3 \/ G0B) is connected by A19, A20, CONNSP_1: 1, CONNSP_1: 17;

            G0B c= (C3 \/ G0B) by XBOOLE_1: 7;

            then G0B = (C3 \/ G0B) by A11, A22;

            then C3 c= G0B by XBOOLE_1: 7;

            hence C3 = G0A or C3 = G0B by A12, A21;

          end;

        end;

        hence C3 = G0A or C3 = G0B;

      end;

      hence thesis by A2, A3, A4, A10, A11;

    end;

    theorem :: JORDAN1:43

    for s1, s2, t1, t2 holds for P be Subset of ( TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p be 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 be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 }, P2 = { pc where pc be 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 Th23, Th24;

      reconsider PC = (P ` ) as Subset of ( TOP-REAL 2);

      

       A4: P1 = { pa where pa be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 };

      

       A5: P2 = { pc where pc be 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, Th30;

      

       A7: PC <> {} by A1, A2, A3, A4, A5, Th30;

      

       A8: P1 misses P2 by A1, A2, A3, Th30;

      

       A9: P = (( Cl P1) \ P1) by A1, A2, A3, A5, Th31;

      

       A10: P = (( Cl P2) \ P2) by A1, A2, A3, A4, Th31;

      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, Th30;

      hence thesis by A6, A7, A8, A9, A10;

    end;

    theorem :: JORDAN1:44

    for s1, t1, s2, t2 holds for P,P2 be Subset of ( TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p be 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 be 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 :: JORDAN1:45

    for s1, t1, s2, t2 holds for P,P1 be Subset of ( TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p be 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 be Point of ( TOP-REAL 2) : s1 < (pa `1 ) & (pa `1 ) < s2 & t1 < (pa `2 ) & (pa `2 ) < t2 } holds ( Cl P1) = (P \/ P1) by Lm10;

    theorem :: JORDAN1:46

    for p,q be 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;

    

     Lm12: for x0,y0 be Real holds for P be Subset of ( TOP-REAL 2) st P = { |[x, y0]| where x be 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 be 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 be Real such that

       A4: w1 = |[x1, y0]| and

       A5: x1 <= x0 by A1, A2;

      consider x2 be Real such that

       A6: w2 = |[x2, y0]| and

       A7: x2 <= x0 by A1, A3;

      let v be object;

      assume

       A8: v in ( LSeg (w1,w2));

      then

      reconsider v1 = v as Point of ( TOP-REAL 2);

      consider l be 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 be Real holds for P be Subset of ( TOP-REAL 2) st P = { |[x0, y]| where y be 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 be 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 be Real such that

       A4: w1 = |[x0, y1]| and

       A5: y1 <= y0 by A1, A2;

      consider y2 be Real such that

       A6: w2 = |[x0, y2]| and

       A7: y2 <= y0 by A1, A3;

      let v be object;

      assume

       A8: v in ( LSeg (w1,w2));

      then

      reconsider v1 = v as Point of ( TOP-REAL 2);

      consider l be 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 be Real holds for P be Subset of ( TOP-REAL 2) st P = { |[x, y0]| where x be 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 be 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 be Real such that

       A4: w1 = |[x1, y0]| and

       A5: x1 >= x0 by A1, A2;

      consider x2 be Real such that

       A6: w2 = |[x2, y0]| and

       A7: x2 >= x0 by A1, A3;

      let v be object;

      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 be Real : 0 <= l & l <= 1 } by A8, RLTOPSP1:def 2;

      then

      consider l be 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 be Real holds for P be Subset of ( TOP-REAL 2) st P = { |[x0, y]| where y be 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 be 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 be Real such that

       A4: w1 = |[x0, x1]| and

       A5: x1 >= y0 by A1, A2;

      consider x2 be Real such that

       A6: w2 = |[x0, x2]| and

       A7: x2 >= y0 by A1, A3;

      let v be object;

      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 be Real : 0 <= l & l <= 1 } by A8, RLTOPSP1:def 2;

      then

      consider l be 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 be 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 be 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 be 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 be Real : r <= (p `1 ) } by TOPREAL1: 37;

        hence thesis by Lm12;

      end;

    end