fintopo6.miz



    begin

    reserve FT for non empty RelStr,

A,B,C for Subset of FT;

    registration

      let FT;

      cluster empty -> connected for Subset of FT;

      coherence ;

    end

    ::$Canceled

    theorem :: FINTOPO6:2

    

     Th1: (( {} FT) ^b ) = {}

    proof

      assume not thesis;

      then

      consider x be object such that

       A1: x in (( {} FT) ^b ) by XBOOLE_0:def 1;

      ex y be Element of FT st x = y & ( U_FT y) meets ( {} FT) by A1;

      hence contradiction;

    end;

    registration

      let FT;

      cluster (( {} FT) ^b ) -> empty;

      coherence by Th1;

    end

    theorem :: FINTOPO6:3

    for A be Subset of FT st for B,C be Subset of FT st A = (B \/ C) & B <> {} & C <> {} & B misses C holds (B ^b ) meets C & B meets (C ^b ) holds A is connected;

    definition

      let FT be non empty RelStr;

      :: FINTOPO6:def1

      attr FT is connected means ( [#] FT) is connected;

    end

    theorem :: FINTOPO6:4

    

     Th3: for A be Subset of FT holds A is connected implies for A2,B2 be Subset of FT st A = (A2 \/ B2) & A2 misses B2 & (A2,B2) are_separated holds A2 = ( {} FT) or B2 = ( {} FT)

    proof

      let A be Subset of FT;

      assume

       A1: A is connected;

      let A2,B2 be Subset of FT;

      assume that

       A2: A = (A2 \/ B2) & A2 misses B2 and

       A3: (A2,B2) are_separated ;

      (A2 ^b ) misses B2 by A3, FINTOPO4:def 1;

      hence thesis by A1, A2;

    end;

    theorem :: FINTOPO6:5

    

     Th4: FT is connected implies for A,B be Subset of FT st ( [#] FT) = (A \/ B) & A misses B & (A,B) are_separated holds A = ( {} FT) or B = ( {} FT)

    proof

      assume FT is connected;

      then

       A1: ( [#] FT) is connected;

      let A,B be Subset of FT;

      assume that

       A2: ( [#] FT) = (A \/ B) & A misses B and

       A3: (A,B) are_separated ;

      (A ^b ) misses B by A3, FINTOPO4:def 1;

      hence thesis by A1, A2;

    end;

    theorem :: FINTOPO6:6

    

     Th5: for A,B be Subset of FT st FT is symmetric & (A ^b ) misses B holds A misses (B ^b )

    proof

      let A,B be Subset of FT;

      assume that

       A1: FT is symmetric and

       A2: (A ^b ) misses B;

      assume A meets (B ^b );

      then

      consider x be object such that

       A3: x in A and

       A4: x in (B ^b ) by XBOOLE_0: 3;

      consider y be Element of FT such that

       A5: x = y and

       A6: ( U_FT y) meets B by A4;

      consider z be object such that

       A7: z in ( U_FT y) and

       A8: z in B by A6, XBOOLE_0: 3;

      reconsider z2 = z as Element of FT by A7;

      y in ( U_FT z2) by A1, A7;

      then ( U_FT z2) meets A by A3, A5, XBOOLE_0: 3;

      then

       A9: z in (A ^b );

      ((A ^b ) /\ B) = {} by A2;

      hence contradiction by A8, A9, XBOOLE_0:def 4;

    end;

    theorem :: FINTOPO6:7

    

     Th6: for A be Subset of FT st FT is symmetric & for A2,B2 be Subset of FT st A = (A2 \/ B2) & A2 misses B2 & (A2,B2) are_separated holds A2 = ( {} FT) or B2 = ( {} FT) holds A is connected

    proof

      let A be Subset of FT;

      assume

       A1: FT is symmetric;

      assume

       A2: for A2,B2 be Subset of FT st A = (A2 \/ B2) & A2 misses B2 & (A2,B2) are_separated holds A2 = ( {} FT) or B2 = ( {} FT);

      for B,C be Subset of FT st A = (B \/ C) & B <> {} & C <> {} & B misses C holds (B ^b ) meets C & B meets (C ^b )

      proof

        let B,C be Subset of FT;

        assume A = (B \/ C) & B <> {} & C <> {} & B misses C;

        then not (B,C) are_separated by A2;

        then not ((B ^b ) misses C & B misses (C ^b )) by FINTOPO4:def 1;

        hence thesis by A1, Th5;

      end;

      hence thesis;

    end;

    definition

      let T be RelStr;

      :: FINTOPO6:def2

      mode SubSpace of T -> RelStr means

      : Def2: the carrier of it c= the carrier of T & for x be Element of it st x in the carrier of it holds ( U_FT x) = (( Im (the InternalRel of T,x)) /\ the carrier of it );

      existence

      proof

        for x be Element of T st x in the carrier of T holds ( U_FT x) = (( Im (the InternalRel of T,x)) /\ the carrier of T) by XBOOLE_1: 28;

        hence thesis;

      end;

    end

    

     Lm1: for T be RelStr holds the RelStr of T is SubSpace of T

    proof

      let T be RelStr;

      set S = the RelStr of T;

      for x be Element of S st x in the carrier of S holds ( U_FT x) = (( Im (the InternalRel of T,x)) /\ the carrier of T) by XBOOLE_1: 28;

      hence thesis by Def2;

    end;

    registration

      let T be RelStr;

      cluster strict for SubSpace of T;

      existence

      proof

         the RelStr of T is SubSpace of T by Lm1;

        hence thesis;

      end;

    end

    registration

      let T be non empty RelStr;

      cluster strict non empty for SubSpace of T;

      existence

      proof

         the RelStr of T is SubSpace of T & the RelStr of T is non empty by Lm1;

        hence thesis;

      end;

    end

    definition

      let T be non empty RelStr, P be non empty Subset of T;

      :: FINTOPO6:def3

      func T | P -> strict non empty SubSpace of T means

      : Def3: ( [#] it ) = P;

      existence

      proof

        deffunc F( set) = (( Im (the InternalRel of T,$1)) /\ P);

        

         A1: for x be Element of T st x in P holds F(x) c= P by XBOOLE_1: 17;

        consider G be Relation of P such that

         A2: for y be Element of T st y in P holds ( Im (G,y)) = F(y) from RELSET_1:sch 3( A1);

        set FS = RelStr (# P, G #);

        for x be Element of FS st x in the carrier of FS holds ( U_FT x) = (( Im (the InternalRel of T,x)) /\ the carrier of FS) by A2;

        then ( [#] FS) = the carrier of FS & FS is strict non empty SubSpace of T by Def2;

        hence thesis;

      end;

      uniqueness

      proof

        let Z1,Z2 be strict non empty SubSpace of T;

        assume that

         A3: ( [#] Z1) = P and

         A4: ( [#] Z2) = P;

        reconsider R1 = the InternalRel of Z1, R2 = the InternalRel of Z2 as Relation of P by A3, A4;

        for z be set st z in P holds ( Im (R1,z)) = ( Im (R2,z))

        proof

          let z be set;

          assume

           A5: z in P;

          then

          reconsider z1 = z as Element of Z1 by A3;

          reconsider z2 = z as Element of Z2 by A4, A5;

          

          thus ( Im (R1,z)) = ( U_FT z1)

          .= (( Im (the InternalRel of T,z1)) /\ the carrier of Z1) by Def2

          .= ( U_FT z2) by A3, A4, Def2

          .= ( Im (R2,z));

        end;

        hence thesis by A3, A4, RELSET_1: 31;

      end;

    end

    theorem :: FINTOPO6:8

    

     Th7: for X be non empty SubSpace of FT st FT is filled holds X is filled

    proof

      let X be non empty SubSpace of FT;

      assume

       A1: FT is filled;

      let x be Element of X;

      the carrier of X c= the carrier of FT by Def2;

      then

      reconsider x2 = x as Element of FT;

      

       A2: ( U_FT x) = (( U_FT x2) /\ ( [#] X)) by Def2;

      x2 in ( U_FT x2) by A1;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    registration

      let FT be filled non empty RelStr;

      cluster -> filled for non empty SubSpace of FT;

      coherence by Th7;

    end

    theorem :: FINTOPO6:9

    for X be non empty SubSpace of FT st FT is symmetric holds X is symmetric

    proof

      let X be non empty SubSpace of FT;

      assume

       A1: FT is symmetric;

      for x,y be Element of X holds y in ( U_FT x) implies x in ( U_FT y)

      proof

        let x,y be Element of X;

        assume

         A2: y in ( U_FT x);

        the carrier of X c= the carrier of FT by Def2;

        then

        reconsider x2 = x, y2 = y as Element of FT;

        

         A3: ( U_FT x) = (( U_FT x2) /\ ( [#] X)) & ( U_FT y) = (( U_FT y2) /\ ( [#] X)) by Def2;

        y2 in ( U_FT x2) implies x2 in ( U_FT y2) by A1;

        hence thesis by A2, A3, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO6:10

    

     Th9: for X9 be SubSpace of FT, A be Subset of X9 holds A is Subset of FT

    proof

      let X9 be SubSpace of FT, A be Subset of X9;

      the carrier of X9 c= the carrier of FT by Def2;

      hence thesis by XBOOLE_1: 1;

    end;

    theorem :: FINTOPO6:11

    for P be Subset of FT holds P is closed iff (P ` ) is open

    proof

      let P be Subset of FT;

      (P ` ) is open implies ((P ` ) ` ) is closed by FIN_TOPO: 23;

      hence thesis by FIN_TOPO: 24;

    end;

    theorem :: FINTOPO6:12

    for A be Subset of FT holds A is open iff (for z be Element of FT st ( U_FT z) c= A holds z in A) & for x be Element of FT st x in A holds ( U_FT x) c= A

    proof

      let A be Subset of FT;

      hereby

        assume A is open;

        then

         A1: A = (A ^i );

        hence for z be Element of FT st ( U_FT z) c= A holds z in A;

        for x be Element of FT st x in A holds ( U_FT x) c= A

        proof

          let x be Element of FT;

          assume x in A;

          then ex y be Element of FT st x = y & ( U_FT y) c= A by A1;

          hence thesis;

        end;

        hence for x be Element of FT st x in A holds ( U_FT x) c= A;

      end;

      assume that

       A2: for z be Element of FT st ( U_FT z) c= A holds z in A and

       A3: for x be Element of FT st x in A holds ( U_FT x) c= A;

      

       A4: A c= { y where y be Element of FT : ( U_FT y) c= A }

      proof

        let u be object;

        assume

         A5: u in A;

        then

        reconsider y2 = u as Element of FT;

        ( U_FT y2) c= A by A3, A5;

        hence thesis;

      end;

      { y where y be Element of FT : ( U_FT y) c= A } c= A

      proof

        let u be object;

        assume u in { y where y be Element of FT : ( U_FT y) c= A };

        then ex y be Element of FT st y = u & ( U_FT y) c= A;

        hence thesis by A2;

      end;

      then A = (A ^i ) by A4;

      hence thesis;

    end;

    theorem :: FINTOPO6:13

    

     Th12: for X9 be non empty SubSpace of FT, A be Subset of FT, A1 be Subset of X9 st A = A1 holds (A1 ^b ) = ((A ^b ) /\ ( [#] X9))

    proof

      let X9 be non empty SubSpace of FT, A be Subset of FT, A1 be Subset of X9 such that

       A1: A = A1;

      

       A2: ((A ^b ) /\ ( [#] X9)) c= (A1 ^b )

      proof

        let u be object;

        assume

         A3: u in ((A ^b ) /\ ( [#] X9));

        then u in (A ^b ) by XBOOLE_0:def 4;

        then

        consider y2 be Element of FT such that

         A4: u = y2 and

         A5: ( U_FT y2) meets A;

        reconsider y3 = y2 as Element of X9 by A3, A4;

        consider z be object such that

         A6: z in ( U_FT y2) and

         A7: z in A by A5, XBOOLE_0: 3;

        ( U_FT y3) = (( U_FT y2) /\ ( [#] X9)) by Def2;

        then z in ( U_FT y3) by A1, A6, A7, XBOOLE_0:def 4;

        then ( U_FT y3) meets A1 by A1, A7, XBOOLE_0: 3;

        hence thesis by A4;

      end;

      (A1 ^b ) c= ((A ^b ) /\ ( [#] X9))

      proof

        reconsider Y = X9 as non empty RelStr;

        let x be object;

        assume x in (A1 ^b );

        then

        consider y be Element of Y such that

         A8: y = x and

         A9: ( U_FT y) meets A1;

        y in the carrier of X9 & the carrier of Y c= the carrier of FT by Def2;

        then

        reconsider z = y as Element of FT;

        ( U_FT y) = (( Im (the InternalRel of FT,y)) /\ the carrier of X9) by Def2;

        then ( U_FT z) meets A by A1, A9, XBOOLE_1: 74;

        then z in { u where u be Element of FT : ( U_FT u) meets A };

        hence thesis by A8, XBOOLE_0:def 4;

      end;

      hence thesis by A2;

    end;

    theorem :: FINTOPO6:14

    for X9 be non empty SubSpace of FT, P1,Q1 be Subset of FT, P,Q be Subset of X9 st P = P1 & Q = Q1 holds (P,Q) are_separated implies (P1,Q1) are_separated

    proof

      let X9 be non empty SubSpace of FT, P1,Q1 be Subset of FT, P,Q be Subset of X9 such that

       A1: P = P1 & Q = Q1;

      reconsider P2 = P, Q2 = Q as Subset of FT by Th9;

      assume

       A2: (P,Q) are_separated ;

      then (P ^b ) misses Q by FINTOPO4:def 1;

      then

       A3: ((P ^b ) /\ Q) = {} ;

      P misses (Q ^b ) by A2, FINTOPO4:def 1;

      then

       A4: (P /\ (Q ^b )) = {} ;

      (P /\ (Q ^b )) = (P /\ (( [#] X9) /\ (Q2 ^b ))) by Th12

      .= ((P /\ ( [#] X9)) /\ (Q2 ^b )) by XBOOLE_1: 16

      .= (P2 /\ (Q2 ^b )) by XBOOLE_1: 28;

      then

       A5: P2 misses (Q2 ^b ) by A4;

      ((P ^b ) /\ Q) = (((P2 ^b ) /\ ( [#] X9)) /\ Q) by Th12

      .= ((P2 ^b ) /\ (Q /\ ( [#] X9))) by XBOOLE_1: 16

      .= ((P2 ^b ) /\ Q2) by XBOOLE_1: 28;

      then (P2 ^b ) misses Q2 by A3;

      hence thesis by A1, A5, FINTOPO4:def 1;

    end;

    theorem :: FINTOPO6:15

    for X9 be non empty SubSpace of FT, P,Q be Subset of FT, P1,Q1 be Subset of X9 st P = P1 & Q = Q1 & (P \/ Q) c= ( [#] X9) holds (P,Q) are_separated implies (P1,Q1) are_separated

    proof

      let X9 be non empty SubSpace of FT, P,Q be Subset of FT, P1,Q1 be Subset of X9 such that

       A1: P = P1 & Q = Q1 and

       A2: (P \/ Q) c= ( [#] X9);

      P c= (P \/ Q) & Q c= (P \/ Q) by XBOOLE_1: 7;

      then

      reconsider P2 = P, Q2 = Q as Subset of X9 by A2, XBOOLE_1: 1;

      assume

       A3: (P,Q) are_separated ;

      then P misses (Q ^b ) by FINTOPO4:def 1;

      then

       A4: (P /\ (Q ^b )) = {} ;

      (P2 /\ (Q2 ^b )) = (P2 /\ (( [#] X9) /\ (Q ^b ))) by Th12

      .= ((P2 /\ ( [#] X9)) /\ (Q ^b )) by XBOOLE_1: 16

      .= (P /\ (Q ^b )) by XBOOLE_1: 28;

      then

       A5: P2 misses (Q2 ^b ) by A4;

      (P2 ^b ) = ((P ^b ) /\ ( [#] X9)) by Th12;

      

      then

       A6: ((P2 ^b ) /\ Q2) = ((P ^b ) /\ (Q2 /\ ( [#] X9))) by XBOOLE_1: 16

      .= ((P ^b ) /\ Q) by XBOOLE_1: 28;

      (P ^b ) misses Q by A3, FINTOPO4:def 1;

      then ((P ^b ) /\ Q) = {} ;

      then (P2 ^b ) misses Q2 by A6;

      hence thesis by A1, A5, FINTOPO4:def 1;

    end;

    theorem :: FINTOPO6:16

    

     Th15: for A be non empty Subset of FT holds A is connected iff (FT | A) is connected

    proof

      let A be non empty Subset of FT;

      

       A1: ( [#] (FT | A)) = A by Def3;

      thus A is connected implies (FT | A) is connected

      proof

        assume

         A2: A is connected;

        for B2,C2 be Subset of (FT | A) st ( [#] (FT | A)) = (B2 \/ C2) & B2 <> {} & C2 <> {} & B2 misses C2 holds (B2 ^b ) meets C2

        proof

          let B2,C2 be Subset of (FT | A);

          

           A3: (( [#] (FT | A)) /\ C2) = C2 by XBOOLE_1: 28;

          the carrier of (FT | A) = ( [#] (FT | A))

          .= A by Def3;

          then

          reconsider B3 = B2, C3 = C2 as Subset of FT by XBOOLE_1: 1;

          assume ( [#] (FT | A)) = (B2 \/ C2) & B2 <> {} & C2 <> {} & B2 misses C2;

          then

           A4: (B3 ^b ) meets C3 by A1, A2;

          ((B2 ^b ) /\ C2) = (((B3 ^b ) /\ ( [#] (FT | A))) /\ C2) by Th12

          .= ((B3 ^b ) /\ C3) by A3, XBOOLE_1: 16;

          then ((B2 ^b ) /\ C2) <> {} by A4;

          hence thesis;

        end;

        then ( [#] (FT | A)) is connected;

        hence thesis;

      end;

      assume (FT | A) is connected;

      then

       A5: ( [#] (FT | A)) is connected;

      let B,C be Subset of FT;

      assume that

       A6: A = (B \/ C) and

       A7: B <> {} & C <> {} & B misses C;

      

       A8: ( [#] (FT | A)) = A by Def3;

      then

      reconsider B2 = B as Subset of (FT | A) by A6, XBOOLE_1: 7;

      reconsider C2 = C as Subset of (FT | A) by A6, A8, XBOOLE_1: 7;

      (( [#] (FT | A)) /\ C2) = C2 & (B2 ^b ) = ((B ^b ) /\ ( [#] (FT | A))) by Th12, XBOOLE_1: 28;

      then

       A9: ((B ^b ) /\ C) = ((B2 ^b ) /\ C2) by XBOOLE_1: 16;

      (B2 ^b ) meets C2 by A5, A6, A7, A8;

      hence ((B ^b ) /\ C) <> {} by A9;

    end;

    theorem :: FINTOPO6:17

    for FT be filled non empty RelStr, A be non empty Subset of FT st FT is symmetric holds A is connected iff for P,Q be Subset of FT st A = (P \/ Q) & P misses Q & (P,Q) are_separated holds P = ( {} FT) or Q = ( {} FT)

    proof

      let FT be filled non empty RelStr, A be non empty Subset of FT;

      assume

       A1: FT is symmetric;

      now

        assume not A is connected;

        then not (FT | A) is connected by Th15;

        then not ( [#] (FT | A)) is connected;

        then

        consider P,Q be Subset of (FT | A) such that

         A2: ( [#] (FT | A)) = (P \/ Q) and

         A3: P <> {} & Q <> {} and

         A4: P misses Q and

         A5: (P ^b ) misses Q;

        reconsider P1 = P, Q1 = Q as Subset of FT by Th9;

        take P1, Q1;

        thus A = (P1 \/ Q1) & P1 misses Q1 by A2, A4, Def3;

        

         A6: (P ^b ) = ((P1 ^b ) /\ ( [#] (FT | A))) by Th12;

        (( [#] (FT | A)) /\ Q1) = Q1 by XBOOLE_1: 28;

        

        then ((P1 ^b ) /\ Q1) = (((P1 ^b ) /\ ( [#] (FT | A))) /\ Q) by XBOOLE_1: 16

        .= {} by A5, A6;

        then (P1 ^b ) misses Q1;

        hence (P1,Q1) are_separated & P1 <> ( {} FT) & Q1 <> ( {} FT) by A1, A3, FINTOPO4: 10;

      end;

      hence thesis by Th3;

    end;

    theorem :: FINTOPO6:18

    for A be Subset of FT st FT is filled connected & A <> {} & (A ` ) <> {} holds (A ^delta ) <> {}

    proof

      let A be Subset of FT;

      assume that

       A1: FT is filled connected and

       A2: A <> {} & (A ` ) <> {} ;

       A3:

      now

        assume (A ^b ) meets (A ` );

        then

        consider x be object such that

         A4: x in (A ^b ) and

         A5: x in (A ` ) by XBOOLE_0: 3;

        reconsider x as Element of FT by A4;

        x in ( U_FT x) by A1;

        then

         A6: ( U_FT x) meets (A ` ) by A5, XBOOLE_0: 3;

        ( U_FT x) meets A by A4, FIN_TOPO: 8;

        hence ex z be Element of FT st ( U_FT z) meets A & ( U_FT z) meets (A ` ) by A6;

      end;

       A7:

      now

        assume A meets ((A ` ) ^b );

        then

        consider x be object such that

         A8: x in ((A ` ) ^b ) and

         A9: x in A by XBOOLE_0: 3;

        reconsider x as Element of FT by A8;

        x in ( U_FT x) by A1;

        then

         A10: ( U_FT x) meets A by A9, XBOOLE_0: 3;

        ( U_FT x) meets (A ` ) by A8, FIN_TOPO: 8;

        hence ex z be Element of FT st ( U_FT z) meets A & ( U_FT z) meets (A ` ) by A10;

      end;

       {} = ( {} FT) & (A \/ (A ` )) = ( [#] FT) by XBOOLE_1: 45;

      then not (A,(A ` )) are_separated by A1, A2, Th4, XBOOLE_1: 79;

      hence thesis by A3, A7, FINTOPO4:def 1, FIN_TOPO: 5;

    end;

    theorem :: FINTOPO6:19

    for A be Subset of FT st FT is filled symmetric & FT is connected & A <> {} & (A ` ) <> {} holds (A ^deltai ) <> {}

    proof

      let A be Subset of FT;

      assume that

       A1: FT is filled symmetric and

       A2: FT is connected & A <> {} & (A ` ) <> {} ;

       A3:

      now

        assume (A ^b ) meets (A ` );

        then

        consider x be object such that

         A4: x in (A ^b ) and

         A5: x in (A ` ) by XBOOLE_0: 3;

        reconsider x as Element of FT by A4;

        ( U_FT x) meets A by A4, FIN_TOPO: 8;

        then

        consider y be object such that

         A6: y in ( U_FT x) and

         A7: y in A by XBOOLE_0: 3;

        reconsider y as Element of FT by A6;

        y in ( U_FT y) by A1;

        then

         A8: ( U_FT y) meets A by A7, XBOOLE_0: 3;

        x in ( U_FT y) by A1, A6;

        then ( U_FT y) meets (A ` ) by A5, XBOOLE_0: 3;

        then y in (A ^delta ) by A8;

        hence thesis by A7, XBOOLE_0:def 4;

      end;

       A9:

      now

        assume A meets ((A ` ) ^b );

        then

        consider x be object such that

         A10: x in ((A ` ) ^b ) and

         A11: x in A by XBOOLE_0: 3;

        reconsider x as Element of FT by A10;

        x in ( U_FT x) by A1;

        then

         A12: ( U_FT x) meets A by A11, XBOOLE_0: 3;

        ( U_FT x) meets (A ` ) by A10, FIN_TOPO: 8;

        then x in (A ^delta ) by A12;

        hence thesis by A11, XBOOLE_0:def 4;

      end;

       {} = ( {} FT) & (A \/ (A ` )) = ( [#] FT) by XBOOLE_1: 45;

      then not (A,(A ` )) are_separated by A2, Th4, XBOOLE_1: 79;

      hence thesis by A3, A9, FINTOPO4:def 1;

    end;

    theorem :: FINTOPO6:20

    for A be Subset of FT st FT is filled symmetric & FT is connected & A <> {} & (A ` ) <> {} holds (A ^deltao ) <> {}

    proof

      let A be Subset of FT;

      assume that

       A1: FT is filled symmetric and

       A2: FT is connected & A <> {} & (A ` ) <> {} ;

       A3:

      now

        assume A meets ((A ` ) ^b );

        then

        consider x be object such that

         A4: x in ((A ` ) ^b ) and

         A5: x in A by XBOOLE_0: 3;

        reconsider x as Element of FT by A4;

        ( U_FT x) meets (A ` ) by A4, FIN_TOPO: 8;

        then

        consider y be object such that

         A6: y in ( U_FT x) and

         A7: y in (A ` ) by XBOOLE_0: 3;

        reconsider y as Element of FT by A6;

        y in ( U_FT y) by A1;

        then

         A8: ( U_FT y) meets (A ` ) by A7, XBOOLE_0: 3;

        x in ( U_FT y) by A1, A6;

        then ( U_FT y) meets A by A5, XBOOLE_0: 3;

        then y in (A ^delta ) by A8;

        hence thesis by A7, XBOOLE_0:def 4;

      end;

       A9:

      now

        assume (A ^b ) meets (A ` );

        then

        consider x be object such that

         A10: x in (A ^b ) and

         A11: x in (A ` ) by XBOOLE_0: 3;

        reconsider x as Element of FT by A10;

        x in ( U_FT x) by A1;

        then

         A12: ( U_FT x) meets (A ` ) by A11, XBOOLE_0: 3;

        ( U_FT x) meets A by A10, FIN_TOPO: 8;

        then x in (A ^delta ) by A12;

        hence thesis by A11, XBOOLE_0:def 4;

      end;

       {} = ( {} FT) & (A \/ (A ` )) = ( [#] FT) by XBOOLE_1: 45;

      then not (A,(A ` )) are_separated by A2, Th4, XBOOLE_1: 79;

      hence thesis by A9, A3, FINTOPO4:def 1;

    end;

    theorem :: FINTOPO6:21

    for A be Subset of FT holds (A ^deltai ) misses (A ^deltao )

    proof

      let A be Subset of FT;

      A misses (A ` ) by XBOOLE_1: 79;

      then

       A1: (A /\ (A ` )) = {} ;

      

      thus ((A ^deltai ) /\ (A ^deltao )) = ((A /\ ((A ^delta ) /\ (A ` ))) /\ (A ^delta )) by XBOOLE_1: 16

      .= (((A /\ (A ` )) /\ (A ^delta )) /\ (A ^delta )) by XBOOLE_1: 16

      .= {} by A1;

    end;

    theorem :: FINTOPO6:22

    for FT be filled non empty RelStr, A be Subset of FT holds (A ^deltao ) = ((A ^b ) \ A)

    proof

      let FT be filled non empty RelStr, A be Subset of FT;

      

       A1: ((A ` ) /\ ((A ` ) ^b )) = (A ` ) by FIN_TOPO: 13, XBOOLE_1: 28;

      

      thus (A ^deltao ) = ((A ` ) /\ ((A ^b ) /\ ((A ` ) ^b ))) by FIN_TOPO: 18

      .= ((A ^b ) /\ ((A ` ) /\ ((A ` ) ^b ))) by XBOOLE_1: 16

      .= ((A ^b ) \ A) by A1, SUBSET_1: 13;

    end;

    theorem :: FINTOPO6:23

    for A,B be Subset of FT st (A,B) are_separated holds (A ^deltao ) misses B

    proof

      let A,B be Subset of FT;

      assume (A,B) are_separated ;

      then

       A1: (A ^b ) misses B by FINTOPO4:def 1;

      

      thus ((A ^deltao ) /\ B) = ((A ` ) /\ ((A ^delta ) /\ B)) by XBOOLE_1: 16

      .= ((A ` ) /\ (((A ^b ) /\ ((A ` ) ^b )) /\ B)) by FIN_TOPO: 18

      .= ((A ` ) /\ (((A ` ) ^b ) /\ ((A ^b ) /\ B))) by XBOOLE_1: 16

      .= ((A ` ) /\ (((A ` ) ^b ) /\ {} )) by A1

      .= {} ;

    end;

    theorem :: FINTOPO6:24

    for A,B be Subset of FT st FT is filled & A misses B & (A ^deltao ) misses B & (B ^deltao ) misses A holds (A,B) are_separated

    proof

      let A,B be Subset of FT;

      assume that

       A1: FT is filled and

       A2: (A /\ B) = {} and

       A3: ((A ^deltao ) /\ B) = {} and

       A4: ((B ^deltao ) /\ A) = {} ;

      ((B ` ) /\ ((B ^delta ) /\ A)) = {} by A4, XBOOLE_1: 16;

      then ((B ` ) /\ (((B ^b ) /\ ((B ` ) ^b )) /\ A)) = {} by FIN_TOPO: 18;

      then ((B ` ) /\ (((B ` ) ^b ) /\ ((B ^b ) /\ A))) = {} by XBOOLE_1: 16;

      then

       A5: (((B ` ) /\ ((B ` ) ^b )) /\ ((B ^b ) /\ A)) = {} by XBOOLE_1: 16;

      ((B ` ) /\ ((B ` ) ^b )) = (B ` ) by A1, FIN_TOPO: 13, XBOOLE_1: 28;

      then (B ` ) misses ((B ^b ) /\ A) by A5;

      then ((B ^b ) /\ A) c= B by SUBSET_1: 24;

      then (((B ^b ) /\ A) /\ A) c= (B /\ A) by XBOOLE_1: 26;

      then ((B ^b ) /\ (A /\ A)) c= (B /\ A) by XBOOLE_1: 16;

      then ((B ^b ) /\ A) = {} by A2, XBOOLE_1: 3;

      then

       A6: A misses (B ^b );

      ((A ` ) /\ ((A ^delta ) /\ B)) = {} by A3, XBOOLE_1: 16;

      then ((A ` ) /\ (((A ^b ) /\ ((A ` ) ^b )) /\ B)) = {} by FIN_TOPO: 18;

      then ((A ` ) /\ (((A ` ) ^b ) /\ ((A ^b ) /\ B))) = {} by XBOOLE_1: 16;

      then

       A7: (((A ` ) /\ ((A ` ) ^b )) /\ ((A ^b ) /\ B)) = {} by XBOOLE_1: 16;

      ((A ` ) /\ ((A ` ) ^b )) = (A ` ) by A1, FIN_TOPO: 13, XBOOLE_1: 28;

      then (A ` ) misses ((A ^b ) /\ B) by A7;

      then ((A ^b ) /\ B) c= A by SUBSET_1: 24;

      then (((A ^b ) /\ B) /\ B) c= (A /\ B) by XBOOLE_1: 26;

      then ((A ^b ) /\ (B /\ B)) c= (A /\ B) by XBOOLE_1: 16;

      then ((A ^b ) /\ B) = {} by A2, XBOOLE_1: 3;

      then (A ^b ) misses B;

      hence thesis by A6, FINTOPO4:def 1;

    end;

    theorem :: FINTOPO6:25

    

     Th24: for x be Point of FT holds {x} is connected

    proof

      let x be Point of FT;

      assume not {x} is connected;

      then

      consider P,Q be Subset of FT such that

       A1: {x} = (P \/ Q) and

       A2: P <> {} and

       A3: Q <> {} and

       A4: P misses Q and not ((P ^b ) meets Q & P meets (Q ^b ));

      P <> Q by A2, A4;

      hence contradiction by A1, A2, A3, ZFMISC_1: 38;

    end;

    registration

      let FT;

      let x be Point of FT;

      cluster {x} -> connected;

      coherence by Th24;

    end

    definition

      let FT be non empty RelStr, A be Subset of FT;

      :: FINTOPO6:def4

      pred A is_a_component_of FT means A is connected & for B be Subset of FT st B is connected holds A c= B implies A = B;

    end

    theorem :: FINTOPO6:26

    for A be Subset of FT st A is_a_component_of FT holds A <> ( {} FT)

    proof

      let A be Subset of FT;

      set x = the Point of FT;

       {} c= {x};

      hence thesis;

    end;

    theorem :: FINTOPO6:27

    A is closed & B is closed & A misses B implies (A,B) are_separated by FINTOPO4:def 1;

    theorem :: FINTOPO6:28

    

     Th27: FT is filled & ( [#] FT) = (A \/ B) & (A,B) are_separated implies A is open closed

    proof

      assume that

       A1: FT is filled and

       A2: ( [#] FT) = (A \/ B) and

       A3: (A,B) are_separated ;

      B c= (B ^b ) by A1, FIN_TOPO: 13;

      then A misses (B ^b ) implies (B ^b ) = B by A2, XBOOLE_1: 73;

      then

       A4: B is closed by A3, FINTOPO4:def 1;

      A c= (A ^b ) by A1, FIN_TOPO: 13;

      then

       A5: (A ^b ) misses B implies (A ^b ) = A by A2, XBOOLE_1: 73;

      (B ` ) = A by A1, A2, A3, FINTOPO4: 6, PRE_TOPC: 5;

      hence thesis by A3, A5, A4, FINTOPO4:def 1, FIN_TOPO: 24;

    end;

    theorem :: FINTOPO6:29

    

     Th28: for A,B,A1,B1 be Subset of FT holds (A,B) are_separated & A1 c= A & B1 c= B implies (A1,B1) are_separated

    proof

      let A,B,A1,B1 be Subset of FT;

      assume that

       A1: (A,B) are_separated and

       A2: A1 c= A and

       A3: B1 c= B;

      A misses (B ^b ) by A1, FINTOPO4:def 1;

      then

       A4: (A /\ (B ^b )) = {} ;

      (B1 ^b ) c= (B ^b ) by A3, FIN_TOPO: 14;

      then (A1 /\ (B1 ^b )) = ( {} FT) by A2, A4, XBOOLE_1: 3, XBOOLE_1: 27;

      then

       A5: A1 misses (B1 ^b );

      (A ^b ) misses B by A1, FINTOPO4:def 1;

      then

       A6: ((A ^b ) /\ B) = {} ;

      (A1 ^b ) c= (A ^b ) by A2, FIN_TOPO: 14;

      then ((A1 ^b ) /\ B1) = ( {} FT) by A3, A6, XBOOLE_1: 3, XBOOLE_1: 27;

      then (A1 ^b ) misses B1;

      hence thesis by A5, FINTOPO4:def 1;

    end;

    theorem :: FINTOPO6:30

    

     Th29: (A,B) are_separated & (A,C) are_separated implies (A,(B \/ C)) are_separated

    proof

      assume that

       A1: (A,B) are_separated and

       A2: (A,C) are_separated ;

      

       A3: (A ^b ) misses C by A2, FINTOPO4:def 1;

      (A ^b ) misses B by A1, FINTOPO4:def 1;

      then

       A4: ((A ^b ) /\ B) = {} ;

      ((A ^b ) /\ (B \/ C)) = (((A ^b ) /\ B) \/ ((A ^b ) /\ C)) by XBOOLE_1: 23

      .= {} by A3, A4;

      then

       A5: (A ^b ) misses (B \/ C);

      A misses (B ^b ) by A1, FINTOPO4:def 1;

      then

       A6: (A /\ (B ^b )) = {} ;

      

       A7: A misses (C ^b ) by A2, FINTOPO4:def 1;

      (A /\ ((B \/ C) ^b )) = (A /\ ((B ^b ) \/ (C ^b ))) by FINTOPO3: 8

      .= ((A /\ (B ^b )) \/ (A /\ (C ^b ))) by XBOOLE_1: 23

      .= {} by A7, A6;

      then A misses ((B \/ C) ^b );

      hence thesis by A5, FINTOPO4:def 1;

    end;

    theorem :: FINTOPO6:31

    FT is filled symmetric & (for A,B be Subset of FT st ( [#] FT) = (A \/ B) & A <> ( {} FT) & B <> ( {} FT) & A is closed & B is closed holds A meets B) implies FT is connected

    proof

      assume

       A1: FT is filled symmetric;

      assume

       A2: for A,B be Subset of FT st ( [#] FT) = (A \/ B) & A <> ( {} FT) & B <> ( {} FT) & A is closed & B is closed holds A meets B;

      assume not FT is connected;

      then not ( [#] FT) is connected;

      then

      consider P,Q be Subset of FT such that

       A3: ( [#] FT) = (P \/ Q) and

       A4: P misses Q and

       A5: (P,Q) are_separated and

       A6: P <> ( {} FT) & Q <> ( {} FT) by A1, Th6;

      P is closed & Q is closed by A1, A3, A5, Th27;

      hence contradiction by A2, A3, A4, A6;

    end;

    theorem :: FINTOPO6:32

    FT is connected implies for A,B be Subset of FT st ( [#] FT) = (A \/ B) & A <> ( {} FT) & B <> ( {} FT) & A is closed & B is closed holds A meets B

    proof

      assume

       A1: ( [#] FT) is connected;

      given A,B be Subset of FT such that

       A2: ( [#] FT) = (A \/ B) & A <> ( {} FT) & B <> ( {} FT) & A is closed & B is closed & A misses B;

      thus contradiction by A1, A2;

    end;

    theorem :: FINTOPO6:33

    

     Th32: FT is filled & A is connected & A c= (B \/ C) & (B,C) are_separated implies A c= B or A c= C

    proof

      assume that

       A1: FT is filled and

       A2: A is connected and

       A3: A c= (B \/ C) and

       A4: (B,C) are_separated ;

      

       A5: ((A /\ B) \/ (A /\ C)) = (A /\ (B \/ C)) by XBOOLE_1: 23

      .= A by A3, XBOOLE_1: 28;

      assume that

       A6: not A c= B and

       A7: not A c= C;

      A meets B by A3, A7, XBOOLE_1: 73;

      then

       A8: (A /\ B) <> {} ;

      A meets C by A3, A6, XBOOLE_1: 73;

      then

       A9: (A /\ C) <> {} ;

      

       A10: (A /\ B) c= B & (A /\ C) c= C by XBOOLE_1: 17;

      then ( {} FT) = {} & (A /\ B) misses (A /\ C) by A1, A4, Th28, FINTOPO4: 6;

      hence contradiction by A2, A4, A8, A9, A10, A5, Th3, Th28;

    end;

    theorem :: FINTOPO6:34

    

     Th33: for A,B be Subset of FT st FT is symmetric & A is connected & B is connected & not (A,B) are_separated holds (A \/ B) is connected

    proof

      let A,B be Subset of FT;

      assume that

       A1: FT is symmetric and

       A2: A is connected and

       A3: B is connected and

       A4: not (A,B) are_separated ;

      given P,Q be Subset of FT such that

       A5: (A \/ B) = (P \/ Q) and

       A6: P <> {} and

       A7: Q <> {} and

       A8: P misses Q and

       A9: (P ^b ) misses Q;

      set P2 = (A /\ P), Q2 = (A /\ Q);

      

       A10: P2 misses Q2 by A8, XBOOLE_1: 76;

      

       A11: (Q ^b ) misses P by A1, A9, Th5;

       A12:

      now

        assume that

         A13: A c= Q and

         A14: B c= P;

        per cases by A4, FINTOPO4:def 1;

          suppose (A ^b ) meets B;

          then (Q ^b ) meets B by A13, FIN_TOPO: 14, XBOOLE_1: 63;

          hence contradiction by A11, A14, XBOOLE_1: 63;

        end;

          suppose A meets (B ^b );

          then not (A ^b ) misses B by A1, Th5;

          then (Q ^b ) meets B by A13, FIN_TOPO: 14, XBOOLE_1: 63;

          hence contradiction by A11, A14, XBOOLE_1: 63;

        end;

      end;

       A15:

      now

        assume

         A16: (A /\ P) = {} ;

        

        then

         A17: (A /\ Q) = ((A /\ P) \/ (A /\ Q))

        .= (A /\ (P \/ Q)) by XBOOLE_1: 23

        .= A by A5, XBOOLE_1: 21;

         A18:

        now

          assume (B /\ Q) = {} ;

          

          then (B /\ P) = ((B /\ Q) \/ (B /\ P))

          .= (B /\ (Q \/ P)) by XBOOLE_1: 23

          .= B by A5, XBOOLE_1: 21;

          hence contradiction by A12, A17, XBOOLE_1: 18;

        end;

        set P3 = (B /\ P), Q3 = (B /\ Q);

        

         A19: (P3 \/ Q3) = (B /\ (P \/ Q)) by XBOOLE_1: 23

        .= B by A5, XBOOLE_1: 21;

        

         A20: P3 misses Q3 by A8, XBOOLE_1: 76;

        (P3 ^b ) c= (P ^b ) & Q3 c= Q by FIN_TOPO: 14, XBOOLE_1: 17;

        then

         A21: (P3 ^b ) misses Q3 by A9, XBOOLE_1: 64;

        (B /\ P) = ((A /\ P) \/ (B /\ P)) by A16

        .= ((A \/ B) /\ P) by XBOOLE_1: 23

        .= P by A5, XBOOLE_1: 21;

        hence contradiction by A3, A6, A18, A19, A20, A21;

      end;

       A22:

      now

        assume that

         A23: A c= P and

         A24: B c= Q;

        

         A25: (A ^b ) c= (P ^b ) by A23, FIN_TOPO: 14;

        per cases by A4, FINTOPO4:def 1;

          suppose (A ^b ) meets B;

          hence contradiction by A9, A24, A25, XBOOLE_1: 64;

        end;

          suppose A meets (B ^b );

          then not (A ^b ) misses B by A1, Th5;

          hence contradiction by A9, A24, A25, XBOOLE_1: 64;

        end;

      end;

       A26:

      now

        assume

         A27: (A /\ Q) = {} ;

        

        then

         A28: (A /\ P) = ((A /\ Q) \/ (A /\ P))

        .= (A /\ (Q \/ P)) by XBOOLE_1: 23

        .= A by A5, XBOOLE_1: 21;

         A29:

        now

          assume (B /\ P) = {} ;

          

          then (B /\ Q) = ((B /\ P) \/ (B /\ Q))

          .= (B /\ (P \/ Q)) by XBOOLE_1: 23

          .= B by A5, XBOOLE_1: 21;

          hence contradiction by A22, A28, XBOOLE_1: 18;

        end;

        set P3 = (B /\ Q), Q3 = (B /\ P);

        

         A30: (Q3 \/ P3) = (B /\ (P \/ Q)) by XBOOLE_1: 23

        .= B by A5, XBOOLE_1: 21;

        

         A31: P3 misses Q3 by A8, XBOOLE_1: 76;

        (P3 ^b ) c= (Q ^b ) & Q3 c= P by FIN_TOPO: 14, XBOOLE_1: 17;

        then

         A32: (P3 ^b ) misses Q3 by A11, XBOOLE_1: 64;

        (B /\ Q) = ((A /\ Q) \/ (B /\ Q)) by A27

        .= ((A \/ B) /\ Q) by XBOOLE_1: 23

        .= Q by A5, XBOOLE_1: 21;

        hence contradiction by A3, A7, A29, A30, A31, A32;

      end;

      (P2 ^b ) c= (P ^b ) & Q2 c= Q by FIN_TOPO: 14, XBOOLE_1: 17;

      then

       A33: (P2 ^b ) misses Q2 by A9, XBOOLE_1: 64;

      (P2 \/ Q2) = (A /\ (P \/ Q)) by XBOOLE_1: 23

      .= A by A5, XBOOLE_1: 21;

      hence contradiction by A2, A15, A26, A10, A33;

    end;

    theorem :: FINTOPO6:35

    

     Th34: for A,C be Subset of FT st FT is symmetric & C is connected & C c= A & A c= (C ^b ) holds A is connected

    proof

      let A,C be Subset of FT;

      assume that

       A1: FT is symmetric and

       A2: C is connected and

       A3: C c= A and

       A4: A c= (C ^b );

      let P2,Q2 be Subset of FT;

      assume that

       A5: A = (P2 \/ Q2) and

       A6: P2 <> {} and

       A7: Q2 <> {} and

       A8: P2 misses Q2;

      assume

       A9: not thesis;

      set x2 = the Element of Q2;

      

       A10: x2 in Q2 by A7;

      Q2 c= (Q2 \/ P2) by XBOOLE_1: 7;

      then Q2 c= (C ^b ) by A4, A5;

      then x2 in (C ^b ) by A10;

      then

      consider z2 be Element of FT such that

       A11: z2 = x2 and

       A12: ( U_FT z2) meets C;

      set y3 = the Element of (( U_FT z2) /\ C);

      

       A13: (( U_FT z2) /\ C) <> {} by A12;

      then y3 in (( U_FT z2) /\ C);

      then

      reconsider y4 = y3 as Element of FT;

      y3 in ( U_FT z2) by A13, XBOOLE_0:def 4;

      then z2 in ( U_FT y4) by A1;

      then z2 in (( U_FT y4) /\ Q2) by A7, A11, XBOOLE_0:def 4;

      then

       A14: ( U_FT y4) meets Q2;

      set P3 = (P2 /\ C), Q3 = (Q2 /\ C);

      

       A15: C = (A /\ C) by A3, XBOOLE_1: 28

      .= (P3 \/ Q3) by A5, XBOOLE_1: 23;

      set x = the Element of P2;

      

       A16: x in P2 by A6;

      P2 c= (P2 \/ Q2) by XBOOLE_1: 7;

      then P2 c= (C ^b ) by A4, A5;

      then x in (C ^b ) by A16;

      then

      consider z be Element of FT such that

       A17: z = x and

       A18: ( U_FT z) meets C;

      set y = the Element of (( U_FT z) /\ C);

      

       A19: (( U_FT z) /\ C) <> {} by A18;

      then y in (( U_FT z) /\ C);

      then

      reconsider y2 = y as Element of FT;

      y in ( U_FT z) by A19, XBOOLE_0:def 4;

      then z in ( U_FT y2) by A1;

      then z in (( U_FT y2) /\ P2) by A6, A17, XBOOLE_0:def 4;

      then ( U_FT y2) meets P2;

      then

       A20: y2 in (P2 ^b );

      

       A21: y4 in C by A13, XBOOLE_0:def 4;

       A22:

      now

        assume Q3 = {} ;

        then

         A23: y4 in P2 by A21, A15, XBOOLE_0:def 4;

        consider w be Element of FT such that

         A24: w = y4 and

         A25: ( U_FT w) meets Q2 by A14;

        consider s be object such that

         A26: s in ( U_FT w) and

         A27: s in Q2 by A25, XBOOLE_0: 3;

        reconsider s2 = s as Element of FT by A26;

        w in ( U_FT s2) by A1, A26;

        then ( U_FT s2) meets P2 by A23, A24, XBOOLE_0: 3;

        then s2 in (P2 ^b );

        hence contradiction by A9, A27, XBOOLE_0: 3;

      end;

      

       A28: P3 c= P2 by XBOOLE_1: 17;

      

       A29: y2 in C by A19, XBOOLE_0:def 4;

       A30:

      now

        assume P3 = {} ;

        then y2 in Q2 by A29, A15, XBOOLE_0:def 4;

        then y2 in ((P2 ^b ) /\ Q2) by A20, XBOOLE_0:def 4;

        hence contradiction by A9;

      end;

      P3 misses Q2 by A8, XBOOLE_1: 17, XBOOLE_1: 63;

      then P3 misses Q3 by XBOOLE_1: 17, XBOOLE_1: 63;

      then (P3 ^b ) meets Q3 by A2, A15, A30, A22;

      then (P2 ^b ) meets Q3 by A28, FIN_TOPO: 14, XBOOLE_1: 63;

      hence contradiction by A9, XBOOLE_1: 17, XBOOLE_1: 63;

    end;

    theorem :: FINTOPO6:36

    

     Th35: for C be Subset of FT st FT is filled symmetric & C is connected holds (C ^b ) is connected

    proof

      let C be Subset of FT;

      assume that

       A1: FT is filled symmetric and

       A2: C is connected;

      C c= (C ^b ) by A1, FIN_TOPO: 13;

      hence thesis by A1, A2, Th34;

    end;

    theorem :: FINTOPO6:37

    

     Th36: FT is filled symmetric connected & A is connected & (( [#] FT) \ A) = (B \/ C) & (B,C) are_separated implies (A \/ B) is connected

    proof

      assume that

       A1: FT is filled symmetric and

       A2: FT is connected and

       A3: A is connected and

       A4: (( [#] FT) \ A) = (B \/ C) and

       A5: (B,C) are_separated ;

      

       A6: ( [#] FT) is connected by A2;

      now

        let P,Q be Subset of FT such that

         A7: (A \/ B) = (P \/ Q) and P misses Q and

         A8: (P,Q) are_separated ;

        

         A9: ( [#] FT) = (A \/ (B \/ C)) by A4, XBOOLE_1: 45

        .= ((P \/ Q) \/ C) by A7, XBOOLE_1: 4;

         A10:

        now

          

           A11: ( [#] FT) = (P \/ (Q \/ C)) by A9, XBOOLE_1: 4;

          assume A c= Q;

          then P misses A by A1, A8, Th28, FINTOPO4: 6;

          then P c= B by A7, XBOOLE_1: 7, XBOOLE_1: 73;

          then

           A12: (P,C) are_separated by A5, Th28;

          then P misses (Q \/ C) by A1, A8, Th29, FINTOPO4: 6;

          hence P = ( {} FT) or Q = ( {} FT) by A6, A8, A12, A11, Th3, Th29;

        end;

        now

          

           A13: ( [#] FT) = (Q \/ (P \/ C)) by A9, XBOOLE_1: 4;

          assume A c= P;

          then Q misses A by A1, A8, Th28, FINTOPO4: 6;

          then Q c= B by A7, XBOOLE_1: 7, XBOOLE_1: 73;

          then

           A14: (Q,C) are_separated by A5, Th28;

          then Q misses (P \/ C) by A1, A8, Th29, FINTOPO4: 6;

          hence P = ( {} FT) or Q = ( {} FT) by A6, A8, A14, A13, Th3, Th29;

        end;

        hence P = ( {} FT) or Q = ( {} FT) by A1, A3, A7, A8, A10, Th32, XBOOLE_1: 7;

      end;

      hence thesis by A1, Th6;

    end;

    theorem :: FINTOPO6:38

    

     Th37: for X9 be non empty SubSpace of FT, A be Subset of FT, B be Subset of X9 st A = B holds A is connected iff B is connected

    proof

      let X9 be non empty SubSpace of FT, A8 be Subset of FT, B8 be Subset of X9;

      assume

       A1: A8 = B8;

      per cases ;

        suppose A8 = {} ;

        hence thesis by A1;

      end;

        suppose

         A2: A8 <> {} ;

        then

        reconsider A = A8 as non empty Subset of FT;

        reconsider B = B8 as non empty Subset of X9 by A1, A2;

        reconsider X = X9 as non empty RelStr;

         A3:

        now

          assume not A8 is connected;

          then

          consider P,Q be Subset of FT such that

           A4: A8 = (P \/ Q) and

           A5: P <> {} & Q <> {} & P misses Q and

           A6: (P ^b ) misses Q;

          Q c= A8 by A4, XBOOLE_1: 7;

          then

          reconsider Q9 = Q as Subset of X by A1, XBOOLE_1: 1;

          P c= A8 by A4, XBOOLE_1: 7;

          then

          reconsider P9 = P as Subset of X by A1, XBOOLE_1: 1;

          

           A7: Q9 c= the carrier of X;

          (P9 ^b ) = ((P ^b ) /\ ( [#] X)) by Th12;

          

          then ((P9 ^b ) /\ Q9) = ((P ^b ) /\ (( [#] X) /\ Q)) by XBOOLE_1: 16

          .= ((P ^b ) /\ Q) by A7, XBOOLE_1: 28

          .= {} by A6;

          then (P9 ^b ) misses Q9;

          hence not B8 is connected by A1, A4, A5;

        end;

        now

          assume not B is connected;

          then

          consider P,Q be Subset of X9 such that

           A8: B8 = (P \/ Q) & P <> {} & Q <> {} & P misses Q and

           A9: (P ^b ) misses Q;

          the carrier of X c= the carrier of FT by Def2;

          then

          reconsider Q9 = Q as Subset of FT by XBOOLE_1: 1;

          the carrier of X c= the carrier of FT by Def2;

          then

          reconsider P9 = P as Subset of FT by XBOOLE_1: 1;

          

           A10: (P ^b ) = ((P9 ^b ) /\ ( [#] X)) by Th12;

          ((P9 ^b ) /\ Q9) = ((P9 ^b ) /\ (( [#] X) /\ Q)) by XBOOLE_1: 28

          .= ((P ^b ) /\ Q) by A10, XBOOLE_1: 16

          .= {} by A9;

          then (P9 ^b ) misses Q9;

          hence not A is connected by A1, A8;

        end;

        hence thesis by A3;

      end;

    end;

    theorem :: FINTOPO6:39

    for A be Subset of FT st FT is filled symmetric & A is_a_component_of FT holds A is closed

    proof

      let A be Subset of FT;

      assume that

       A1: FT is filled symmetric and

       A2: A is_a_component_of FT;

      A is connected by A2;

      then

       A3: (A ^b ) is connected by A1, Th35;

      A c= (A ^b ) by A1, FIN_TOPO: 13;

      hence A = (A ^b ) by A2, A3;

    end;

    theorem :: FINTOPO6:40

    

     Th39: for A,B be Subset of FT st FT is symmetric & A is_a_component_of FT & B is_a_component_of FT holds A = B or (A,B) are_separated

    proof

      let A,B be Subset of FT;

      assume that

       A1: FT is symmetric and

       A2: A is_a_component_of FT and

       A3: B is_a_component_of FT;

      

       A4: A is connected by A2;

      assume that

       A5: A <> B and

       A6: not (A,B) are_separated ;

      B is connected by A3;

      then (A \/ B) is connected by A1, A6, A4, Th33;

      then B c= (A \/ B) & A = (A \/ B) by A2, XBOOLE_1: 7;

      hence contradiction by A3, A5, A4;

    end;

    theorem :: FINTOPO6:41

    for A,B be Subset of FT st FT is filled symmetric & A is_a_component_of FT & B is_a_component_of FT holds A = B or A misses B by Th39, FINTOPO4: 6;

    theorem :: FINTOPO6:42

    for C be Subset of FT st FT is filled symmetric & C is connected holds for S be Subset of FT st S is_a_component_of FT holds C misses S or C c= S

    proof

      let C be Subset of FT;

      assume

       A1: FT is filled symmetric & C is connected;

      let S be Subset of FT;

      assume

       A2: S is_a_component_of FT;

      

       A3: S c= (C \/ S) by XBOOLE_1: 7;

      assume

       A4: C meets S;

      S is connected by A2;

      then (C \/ S) is connected by A1, A4, Th33, FINTOPO4: 6;

      then S = (C \/ S) by A2, A3;

      hence thesis by XBOOLE_1: 7;

    end;

    definition

      let FT be non empty RelStr, A be non empty Subset of FT, B be Subset of FT;

      :: FINTOPO6:def5

      pred B is_a_component_of A means ex B1 be Subset of (FT | A) st B1 = B & B1 is_a_component_of (FT | A);

    end

    theorem :: FINTOPO6:43

    for D be non empty Subset of FT st FT is filled symmetric & D = (( [#] FT) \ A) holds FT is connected & A is connected & C is_a_component_of D implies (( [#] FT) \ C) is connected

    proof

      let D be non empty Subset of FT;

      assume that

       A1: FT is filled symmetric and

       A2: D = (( [#] FT) \ A) and

       A3: FT is connected and

       A4: A is connected and

       A5: C is_a_component_of D;

      consider C1 be Subset of (FT | D) such that

       A6: C1 = C and

       A7: C1 is_a_component_of (FT | D) by A5;

      reconsider C2 = C1 as Subset of FT by A6;

      C1 c= ( [#] (FT | D));

      then C1 c= (( [#] FT) \ A) by A2, Def3;

      then

       A8: ((( [#] FT) \ A) ` ) c= (C2 ` ) by SUBSET_1: 12;

      then

       A9: A c= (C2 ` ) by PRE_TOPC: 3;

      

       A10: A c= (( [#] FT) \ C2) by A8, PRE_TOPC: 3;

      

       A11: C1 is connected by A7;

      now

        A misses C1 by A9, SUBSET_1: 23;

        then

         A12: (A /\ C1) = {} ;

        let P,Q be Subset of FT such that

         A13: (( [#] FT) \ C) = (P \/ Q) and

         A14: P misses Q and

         A15: (P,Q) are_separated ;

        

         A16: C is connected by A6, A11, Th37;

         A17:

        now

          assume

           A18: A c= Q;

          P c= (Q ` ) by A14, SUBSET_1: 23;

          then Q misses (Q ` ) & (A /\ P) c= (Q /\ (Q ` )) by A18, XBOOLE_1: 27, XBOOLE_1: 79;

          then

           A19: (A /\ P) c= {} ;

          ((C \/ P) /\ A) = ((A /\ C) \/ (A /\ P)) by XBOOLE_1: 23

          .= {} by A6, A12, A19, XBOOLE_1: 3;

          then (C \/ P) misses A;

          then (C \/ P) c= (A ` ) by SUBSET_1: 23;

          then (C \/ P) c= ( [#] (FT | D)) by A2, Def3;

          then

          reconsider C1P1 = (C \/ P) as Subset of (FT | D);

          (C \/ P) is connected by A1, A3, A13, A15, A16, Th36;

          then

           A20: C1P1 is connected by Th37;

          C c= (C1 \/ P) by A6, XBOOLE_1: 7;

          then C1P1 = C1 by A6, A7, A20;

          then

           A21: P c= C by A6, XBOOLE_1: 7;

          P c= (( [#] FT) \ C) by A13, XBOOLE_1: 7;

          then C misses (C ` ) & P c= (C /\ (( [#] FT) \ C)) by A21, XBOOLE_1: 19, XBOOLE_1: 79;

          then P c= {} ;

          hence P = ( {} FT) by XBOOLE_1: 3;

        end;

        

         A22: P misses (P ` ) by XBOOLE_1: 79;

        

         A23: Q c= (( [#] FT) \ C) by A13, XBOOLE_1: 7;

        now

          assume

           A24: A c= P;

          Q c= (P ` ) by A14, SUBSET_1: 23;

          then (A /\ Q) c= (P /\ (P ` )) by A24, XBOOLE_1: 27;

          then

           A25: (A /\ Q) c= {} by A22;

          ((C \/ Q) /\ A) = ((A /\ C) \/ (A /\ Q)) by XBOOLE_1: 23

          .= {} by A6, A12, A25, XBOOLE_1: 3;

          then (C \/ Q) misses A;

          then (C \/ Q) c= (A ` ) by SUBSET_1: 23;

          then (C \/ Q) c= ( [#] (FT | D)) by A2, Def3;

          then

          reconsider C1Q1 = (C \/ Q) as Subset of (FT | D);

          (C \/ Q) is connected by A1, A3, A13, A15, A16, Th36;

          then

           A26: C1Q1 is connected by Th37;

          C1 c= (C1 \/ Q) by XBOOLE_1: 7;

          then C1Q1 = C1 by A6, A7, A26;

          then Q c= C by A6, XBOOLE_1: 7;

          then C misses (C ` ) & Q c= (C /\ (( [#] FT) \ C)) by A23, XBOOLE_1: 19, XBOOLE_1: 79;

          then Q c= {} ;

          hence Q = ( {} FT) by XBOOLE_1: 3;

        end;

        hence P = ( {} FT) or Q = ( {} FT) by A1, A4, A6, A10, A13, A15, A17, Th32;

      end;

      hence thesis by A1, Th6;

    end;

    begin

    definition

      let FT;

      let f be FinSequence of FT;

      :: FINTOPO6:def6

      attr f is continuous means 1 <= ( len f) & for i be Nat, x1 be Element of FT st 1 <= i & i < ( len f) & x1 = (f . i) holds (f . (i + 1)) in ( U_FT x1);

    end

    

     Lm2: for x be Element of FT holds <*x*> is continuous by FINSEQ_1: 39;

    registration

      let FT;

      let x be Element of FT;

      cluster <*x*> -> continuous;

      coherence by Lm2;

    end

    theorem :: FINTOPO6:44

    

     Th43: for f be FinSequence of FT, x,y be Element of FT st f is continuous & y = (f . ( len f)) & x in ( U_FT y) holds (f ^ <*x*>) is continuous

    proof

      let f be FinSequence of FT, x,y be Element of FT;

      assume that

       A1: f is continuous and

       A2: y = (f . ( len f)) and

       A3: x in ( U_FT y);

      reconsider g = (f ^ <*x*>) as FinSequence of FT;

      

       A4: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      

       A5: ( len <*x*>) = 1 by FINSEQ_1: 39;

      

       A6: for i be Nat, x1 be Element of FT st 1 <= i & i < ( len g) & x1 = (g . i) holds (g . (i + 1)) in ( U_FT x1)

      proof

        let i be Nat, x1 be Element of FT;

        assume that

         A7: 1 <= i and

         A8: i < ( len g) and

         A9: x1 = (g . i);

        (i + 1) <= ( len g) & 1 < (i + 1) by A7, A8, NAT_1: 13;

        then (i + 1) in ( dom g) by FINSEQ_3: 25;

        then (g . (i + 1)) = (g /. (i + 1)) by PARTFUN1:def 6;

        then

        reconsider x2 = (g . (i + 1)) as Element of FT;

        now

          per cases ;

            suppose

             A10: i < ( len f);

            

             A11: 1 <= (i + 1) by NAT_1: 11;

            (i + 1) <= ( len f) by A10, NAT_1: 13;

            then (i + 1) in ( dom f) by A11, FINSEQ_3: 25;

            then

             A12: (g . (i + 1)) = (f . (i + 1)) by FINSEQ_1:def 7;

            i in ( dom f) by A4, A7, A10;

            then (g . i) = (f . i) by FINSEQ_1:def 7;

            hence x2 in ( U_FT x1) by A1, A7, A9, A10, A12;

          end;

            suppose

             A13: i >= ( len f);

            ( len g) = (( len f) + 1) by A5, FINSEQ_1: 22;

            then

             A14: i <= ( len f) by A8, NAT_1: 13;

            then

             A15: i = ( len f) by A13, XXREAL_0: 1;

            i in ( dom f) by A4, A7, A14;

            then x1 = y by A2, A9, A15, FINSEQ_1:def 7;

            hence x2 in ( U_FT x1) by A3, A15, FINSEQ_1: 42;

          end;

        end;

        hence thesis;

      end;

      ( len (f ^ <*x*>)) = (( len f) + ( len <*x*>)) by FINSEQ_1: 22

      .= (( len f) + 1) by FINSEQ_1: 39;

      then ( len (f ^ <*x*>)) >= 1 by NAT_1: 11;

      hence thesis by A6;

    end;

    theorem :: FINTOPO6:45

    

     Th44: for f,g be FinSequence of FT st f is continuous & g is continuous & (g . 1) in ( U_FT (f /. ( len f))) holds (f ^ g) is continuous

    proof

      let f,g be FinSequence of FT;

      assume that

       A1: f is continuous and

       A2: g is continuous and

       A3: (g . 1) in ( U_FT (f /. ( len f)));

      

       A4: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      ( len g) >= 1 by A2;

      then ( len (f ^ g)) >= ( 0 + 1) by A4, XREAL_1: 7;

      hence ( len (f ^ g)) >= 1;

      let i be Nat, x1 be Element of FT;

      set g2 = (f ^ g);

      

       A5: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      

       A6: ( len f) >= 1 by A1;

      assume that

       A7: 1 <= i and

       A8: i < ( len (f ^ g)) and

       A9: x1 = ((f ^ g) . i);

      (i + 1) <= ( len g2) & 1 < (i + 1) by A7, A8, NAT_1: 13;

      then (i + 1) in ( dom g2) by FINSEQ_3: 25;

      then (g2 . (i + 1)) = (g2 /. (i + 1)) by PARTFUN1:def 6;

      then

      reconsider x2 = (g2 . (i + 1)) as Element of FT;

      per cases ;

        suppose

         A10: i < ( len f);

        

         A11: 1 <= (i + 1) by NAT_1: 11;

        (i + 1) <= ( len f) by A10, NAT_1: 13;

        then (i + 1) in ( dom f) by A11, FINSEQ_3: 25;

        then

         A12: (g2 . (i + 1)) = (f . (i + 1)) by FINSEQ_1:def 7;

        i in ( dom f) by A5, A7, A10;

        then (g2 . i) = (f . i) by FINSEQ_1:def 7;

        hence thesis by A1, A7, A9, A10, A12;

      end;

        suppose

         A13: i >= ( len f);

        then

         A14: (i + 1) > ( len f) by NAT_1: 13;

        

         A15: i < (( len f) + ( len g)) by A8, FINSEQ_1: 22;

        

         A16: ( len g2) = (( len f) + ( len g)) by FINSEQ_1: 22;

        then

         A17: (i + 1) <= (( len f) + ( len g)) by A8, NAT_1: 13;

        per cases by A13, XXREAL_0: 1;

          suppose

           A18: i = ( len f);

          

           A19: ( len f) in ( dom f) by A6, FINSEQ_3: 25;

          

          then

           A20: x1 = (f . ( len f)) by A9, A18, FINSEQ_1:def 7

          .= (f /. ( len f)) by A19, PARTFUN1:def 6;

          x2 = (g . ((i + 1) - ( len f))) by A14, A16, A17, FINSEQ_1: 24

          .= (g . 1) by A18;

          hence thesis by A3, A20;

        end;

          suppose

           A21: i > ( len f);

          set j = (i -' ( len f));

          

           A22: (i - ( len f)) > 0 by A21, XREAL_1: 50;

          then

           A23: (i -' ( len f)) = (i - ( len f)) by XREAL_0:def 2;

          then (j + 1) = ((i + 1) - ( len f));

          then

           A24: x2 = (g . (j + 1)) by A14, A16, A17, FINSEQ_1: 24;

          

           A25: (i - ( len f)) < ( len g) by A15, XREAL_1: 19;

          i >= (( len f) + 1) by A21, NAT_1: 13;

          then

           A26: x1 = (g . j) by A9, A15, A23, FINSEQ_1: 23;

          (i -' ( len f)) >= ( 0 + 1) by A22, A23, NAT_1: 13;

          hence thesis by A2, A23, A24, A26, A25;

        end;

      end;

    end;

    definition

      let FT;

      let A be Subset of FT;

      :: FINTOPO6:def7

      attr A is arcwise_connected means for x1,x2 be Element of FT st x1 in A & x2 in A holds ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2;

    end

    registration

      let FT;

      cluster empty -> arcwise_connected for Subset of FT;

      coherence ;

    end

    

     Lm3: for x be Element of FT holds {x} is arcwise_connected

    proof

      let x be Element of FT;

      set A = {x};

      

       A1: ( rng <*x*>) c= A by FINSEQ_1: 39;

      

       A2: ( <*x*> . 1) = x by FINSEQ_1: 40;

      then

       A3: ( <*x*> . ( len <*x*>)) = x by FINSEQ_1: 40;

      for x1,x2 be Element of FT st x1 in A & x2 in A holds ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2

      proof

        let x1,x2 be Element of FT;

        assume x1 in A & x2 in A;

        then x1 = x & x2 = x by TARSKI:def 1;

        hence thesis by A2, A3, A1;

      end;

      hence thesis;

    end;

    registration

      let FT;

      let x be Element of FT;

      cluster {x} -> arcwise_connected;

      coherence by Lm3;

    end

    theorem :: FINTOPO6:46

    for A be Subset of FT st FT is symmetric holds A is connected iff A is arcwise_connected

    proof

      let A be Subset of FT;

      assume

       A1: FT is symmetric;

      now

        assume not A is arcwise_connected;

        then

        consider x1,x2 be Element of FT such that

         A2: x1 in A and

         A3: x2 in A and

         A4: not (ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2);

        

         A5: { z where z be Element of FT : z in A & ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = z } c= A

        proof

          let x be object;

          assume x in { z where z be Element of FT : z in A & ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = z };

          then ex z be Element of FT st x = z & z in A & ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = z;

          hence thesis;

        end;

        then

        reconsider G = { z where z be Element of FT : z in A & ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = z } as Subset of FT by XBOOLE_1: 1;

        

         A6: G misses (A \ G) by XBOOLE_1: 79;

         A7:

        now

          assume (G ^b ) meets (A \ G);

          then

          consider u be object such that

           A8: u in (G ^b ) and

           A9: u in (A \ G) by XBOOLE_0: 3;

          

           A10: not u in G by A9, XBOOLE_0:def 5;

          consider x be Element of FT such that

           A11: u = x and

           A12: ( U_FT x) meets G by A8;

          consider y be object such that

           A13: y in ( U_FT x) and

           A14: y in G by A12, XBOOLE_0: 3;

          consider z2 be Element of FT such that

           A15: y = z2 and z2 in A and

           A16: ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = z2 by A14;

          consider f be FinSequence of FT such that

           A17: f is continuous and

           A18: ( rng f) c= A and

           A19: (f . 1) = x1 and

           A20: (f . ( len f)) = z2 by A16;

          reconsider g = (f ^ <*x*>) as FinSequence of FT;

          

           A21: ( rng g) = (( rng f) \/ ( rng <*x*>)) by FINSEQ_1: 31

          .= (( rng f) \/ {x}) by FINSEQ_1: 38;

          

           A22: u in A by A9, XBOOLE_0:def 5;

          then {x} c= A by A11, ZFMISC_1: 31;

          then

           A23: ( rng g) c= A by A18, A21, XBOOLE_1: 8;

          1 <= ( len f) by A17;

          then 1 in ( dom f) by FINSEQ_3: 25;

          then

           A24: (g . (( len f) + 1)) = x & (g . 1) = x1 by A19, FINSEQ_1: 42, FINSEQ_1:def 7;

          x in ( U_FT z2) by A1, A13, A15;

          then

           A25: g is continuous by A17, A20, Th43;

          ( len g) = (( len f) + ( len <*x*>)) by FINSEQ_1: 22

          .= (( len f) + 1) by FINSEQ_1: 39;

          hence contradiction by A22, A10, A11, A25, A24, A23;

        end;

         A26:

        now

           {x1} c= A by A2, ZFMISC_1: 31;

          then

           A27: ( rng <*x1*>) c= A by FINSEQ_1: 38;

          assume

           A28: G = {} ;

          

           A29: ( <*x1*> . 1) = x1 by FINSEQ_1: 40;

          then ( <*x1*> . ( len <*x1*>)) = x1 by FINSEQ_1: 39;

          then x1 in G by A2, A27, A29;

          hence contradiction by A28;

        end;

         A30:

        now

          assume (A \ G) = {} ;

          then A c= G by XBOOLE_1: 37;

          then G = A by A5;

          then ex z be Element of FT st z = x2 & z in A & ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = z by A3;

          hence contradiction by A4;

        end;

        A = (G \/ (A \ G)) by A5, XBOOLE_1: 45;

        hence not A is connected by A30, A26, A6, A7;

      end;

      hence A is connected implies A is arcwise_connected;

      now

        assume not A is connected;

        then

        consider P,Q be Subset of FT such that

         A31: A = (P \/ Q) and

         A32: P <> {} and

         A33: Q <> {} and

         A34: P misses Q and

         A35: (P ^b ) misses Q;

        set q0 = the Element of Q;

        q0 in Q by A33;

        then

        reconsider q1 = q0 as Element of FT;

        set p0 = the Element of P;

        p0 in P by A32;

        then

        reconsider p1 = p0 as Element of FT;

        

         A36: p1 in A & q1 in A by A31, A32, A33, XBOOLE_0:def 3;

        now

          assume A is arcwise_connected;

          then

          consider f be FinSequence of FT such that

           A37: f is continuous and

           A38: ( rng f) c= A and

           A39: (f . 1) = p1 and

           A40: (f . ( len f)) = q1 by A36;

          defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) & (f . $1) in P;

          ( len f) >= 1 by A37;

          then

           A41: ex k be Nat st P[k] by A32, A39;

          

           A42: for k be Nat st P[k] holds k <= ( len f);

          consider i0 be Nat such that

           A43: P[i0] & for n be Nat st P[n] holds n <= i0 from NAT_1:sch 6( A42, A41);

          i0 <> ( len f) by A33, A34, A40, A43, XBOOLE_0: 3;

          then

           A44: i0 < ( len f) by A43, XXREAL_0: 1;

          then

           A45: (i0 + 1) <= ( len f) by NAT_1: 13;

          reconsider u0 = (f . i0) as Element of FT by A43;

          

           A46: 1 < (i0 + 1) by A43, NAT_1: 13;

          then (i0 + 1) in ( dom f) by A45, FINSEQ_3: 25;

          then

           A47: (f . (i0 + 1)) in ( rng f) by FUNCT_1:def 3;

          then

          reconsider z0 = (f . (i0 + 1)) as Element of FT;

          z0 in ( U_FT u0) by A37, A43, A44;

          then (f . i0) in ( U_FT z0) by A1;

          then ( U_FT z0) meets P by A43, XBOOLE_0: 3;

          then

           A48: z0 in (P ^b );

          now

            assume (f . (i0 + 1)) in P;

            then (i0 + 1) <= i0 by A43, A45, A46;

            hence contradiction by NAT_1: 13;

          end;

          then (f . (i0 + 1)) in Q by A31, A38, A47, XBOOLE_0:def 3;

          hence contradiction by A35, A48, XBOOLE_0: 3;

        end;

        hence not A is arcwise_connected;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO6:47

    

     Th46: for g be FinSequence of FT, k be Nat st g is continuous & 1 <= k holds (g | k) is continuous

    proof

      let g be FinSequence of FT, k be Nat;

      assume that

       A1: g is continuous and

       A2: 1 <= k;

      per cases ;

        suppose ( len g) <= k;

        hence thesis by A1, FINSEQ_1: 58;

      end;

        suppose

         A3: k <= ( len g);

        hence ( len (g | k)) >= 1 by A2, FINSEQ_1: 59;

        let i be Nat, x11 be Element of FT;

        assume that

         A4: 1 <= i and

         A5: i < ( len (g | k)) and

         A6: x11 = ((g | k) . i);

        

         A7: ( len (g | k)) = k by A3, FINSEQ_1: 59;

        then

         A8: ((g | k) . i) = (g . i) by A5, FINSEQ_3: 112;

        (i + 1) <= k by A7, A5, NAT_1: 13;

        then

         A9: ((g | k) . (i + 1)) = (g . (i + 1)) by FINSEQ_3: 112;

        i < ( len g) by A3, A7, A5, XXREAL_0: 2;

        hence thesis by A1, A4, A6, A8, A9;

      end;

    end;

    theorem :: FINTOPO6:48

    

     Th47: for g be FinSequence of FT, k be Element of NAT st g is continuous & k < ( len g) holds (g /^ k) is continuous

    proof

      let g be FinSequence of FT, k be Element of NAT ;

      assume that

       A1: g is continuous and

       A2: k < ( len g);

      

       A3: (( len g) - k) > 0 by A2, XREAL_1: 50;

      then

       A4: (( len g) - k) = (( len g) -' k) by XREAL_0:def 2;

      

       A5: ( len (g /^ k)) = (( len g) - k) by A2, RFINSEQ:def 1;

      

       A6: for i be Nat, x11 be Element of FT st 1 <= i & i < ( len (g /^ k)) & x11 = ((g /^ k) . i) holds ((g /^ k) . (i + 1)) in ( U_FT x11)

      proof

        let i be Nat, x11 be Element of FT;

        assume that

         A7: 1 <= i and

         A8: i < ( len (g /^ k)) and

         A9: x11 = ((g /^ k) . i);

        

         A10: 1 <= (1 + i) by NAT_1: 11;

        i in ( dom (g /^ k)) by A7, A8, FINSEQ_3: 25;

        then

         A11: ((g /^ k) . i) = (g . (i + k)) by A2, RFINSEQ:def 1;

        i <= (i + k) by NAT_1: 11;

        then

         A12: ((i + 1) + k) = ((i + k) + 1) & 1 <= (i + k) by A7, XXREAL_0: 2;

        (i + 1) <= (( len g) -' k) by A5, A4, A8, NAT_1: 13;

        then (i + 1) in ( dom (g /^ k)) by A5, A4, A10, FINSEQ_3: 25;

        then

         A13: ((g /^ k) . (i + 1)) = (g . ((i + 1) + k)) by A2, RFINSEQ:def 1;

        (i + k) < ((( len g) - k) + k) by A5, A8, XREAL_1: 6;

        hence thesis by A1, A9, A11, A13, A12;

      end;

      (( len g) -' k) >= ( 0 + 1) by A3, A4, NAT_1: 13;

      hence thesis by A5, A4, A6;

    end;

    definition

      let FT;

      let g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT;

      :: FINTOPO6:def8

      pred g is_minimum_path_in A,x1,x2 means g is continuous & ( rng g) c= A & (g . 1) = x1 & (g . ( len g)) = x2 & for h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = x2 holds ( len g) <= ( len h);

    end

    theorem :: FINTOPO6:49

    for A be Subset of FT, x be Element of FT st x in A holds <*x*> is_minimum_path_in (A,x,x)

    proof

      let A be Subset of FT, x be Element of FT;

      assume

       A1: x in A;

      thus <*x*> is continuous;

       {x} c= A by A1, ZFMISC_1: 31;

      hence ( rng <*x*>) c= A by FINSEQ_1: 38;

      ( len <*x*>) = 1 by FINSEQ_1: 40;

      hence thesis by FINSEQ_1: 40;

    end;

    

     Lm4: for f be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2 holds ex g be FinSequence of FT st g is continuous & ( rng g) c= A & (g . 1) = x1 & (g . ( len g)) = x2 & for h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = x2 holds ( len g) <= ( len h)

    proof

      let f be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT;

      defpred P[ Nat] means ex g be FinSequence of FT st g is continuous & ( rng g) c= A & (g . 1) = x1 & (g . ( len g)) = x2 & $1 = ( len g);

      assume f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2;

      then

       A1: ex k be Nat st P[k];

      ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A1);

      then

      consider k0 be Nat such that

       A2: P[k0] and

       A3: for n be Nat st P[n] holds k0 <= n;

      consider g0 be FinSequence of FT such that

       A4: g0 is continuous & ( rng g0) c= A & (g0 . 1) = x1 & (g0 . ( len g0)) = x2 and

       A5: k0 = ( len g0) by A2;

      for h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = x2 holds ( len g0) <= ( len h) by A3, A5;

      hence thesis by A4;

    end;

    theorem :: FINTOPO6:50

    for A be Subset of FT holds A is arcwise_connected iff for x1,x2 be Element of FT st x1 in A & x2 in A holds ex g be FinSequence of FT st g is_minimum_path_in (A,x1,x2)

    proof

      let A be Subset of FT;

      thus A is arcwise_connected implies for x1,x2 be Element of FT st x1 in A & x2 in A holds ex g be FinSequence of FT st g is_minimum_path_in (A,x1,x2)

      proof

        assume

         A1: A is arcwise_connected;

        thus for x1,x2 be Element of FT st x1 in A & x2 in A holds ex g be FinSequence of FT st g is_minimum_path_in (A,x1,x2)

        proof

          let x1,x2 be Element of FT;

          assume x1 in A & x2 in A;

          then ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2 by A1;

          then

          consider g2 be FinSequence of FT such that

           A2: g2 is continuous & ( rng g2) c= A & (g2 . 1) = x1 & (g2 . ( len g2)) = x2 & for h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = x2 holds ( len g2) <= ( len h) by Lm4;

          g2 is_minimum_path_in (A,x1,x2) by A2;

          hence thesis;

        end;

      end;

      assume

       A3: for x1,x2 be Element of FT st x1 in A & x2 in A holds ex g be FinSequence of FT st g is_minimum_path_in (A,x1,x2);

      for x1,x2 be Element of FT st x1 in A & x2 in A holds ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2

      proof

        let x1,x2 be Element of FT;

        assume x1 in A & x2 in A;

        then

        consider g be FinSequence of FT such that

         A4: g is_minimum_path_in (A,x1,x2) by A3;

        

         A5: (g . 1) = x1 & (g . ( len g)) = x2 by A4;

        g is continuous & ( rng g) c= A by A4;

        hence thesis by A5;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO6:51

    for A be Subset of FT, x1,x2 be Element of FT st ex f be FinSequence of FT st f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2 holds ex g be FinSequence of FT st g is_minimum_path_in (A,x1,x2)

    proof

      let A be Subset of FT, x1,x2 be Element of FT;

      given f be FinSequence of FT such that

       A1: f is continuous & ( rng f) c= A & (f . 1) = x1 & (f . ( len f)) = x2;

      consider g2 be FinSequence of FT such that

       A2: g2 is continuous & ( rng g2) c= A & (g2 . 1) = x1 & (g2 . ( len g2)) = x2 & for h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = x2 holds ( len g2) <= ( len h) by A1, Lm4;

      g2 is_minimum_path_in (A,x1,x2) by A2;

      hence thesis;

    end;

    theorem :: FINTOPO6:52

    

     Th51: for g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT, k be Element of NAT st g is_minimum_path_in (A,x1,x2) & 1 <= k & k <= ( len g) holds (g | k) is continuous & ( rng (g | k)) c= A & ((g | k) . 1) = x1 & ((g | k) . ( len (g | k))) = (g /. k)

    proof

      let g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT, k be Element of NAT ;

      assume that

       A1: g is_minimum_path_in (A,x1,x2) and

       A2: 1 <= k and

       A3: k <= ( len g);

      

       A4: k in ( dom g) by A2, A3, FINSEQ_3: 25;

      g is continuous by A1;

      hence (g | k) is continuous by A2, Th46;

      

       A5: ( rng (g | k)) c= ( rng g) by FINSEQ_5: 19;

      ( rng g) c= A by A1;

      hence ( rng (g | k)) c= A by A5;

      (g . 1) = x1 by A1;

      hence ((g | k) . 1) = x1 by A2, FINSEQ_3: 112;

      ( len (g | k)) = k by A3, FINSEQ_1: 59;

      

      hence ((g | k) . ( len (g | k))) = (g . k) by FINSEQ_3: 112

      .= (g /. k) by A4, PARTFUN1:def 6;

    end;

    theorem :: FINTOPO6:53

    

     Th52: for g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT, k be Element of NAT st g is_minimum_path_in (A,x1,x2) & k < ( len g) holds (g /^ k) is continuous & ( rng (g /^ k)) c= A & ((g /^ k) . 1) = (g /. (1 + k)) & ((g /^ k) . ( len (g /^ k))) = x2

    proof

      let g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT, k be Element of NAT ;

      assume that

       A1: g is_minimum_path_in (A,x1,x2) and

       A2: k < ( len g);

      

       A3: ( len (g /^ k)) = (( len g) - k) by A2, RFINSEQ:def 1;

      g is continuous by A1;

      hence (g /^ k) is continuous by A2, Th47;

      

       A4: ( rng (g /^ k)) c= ( rng g) by FINSEQ_5: 33;

      ( rng g) c= A by A1;

      hence ( rng (g /^ k)) c= A by A4;

      

       A5: ( len (g /^ k)) = (( len g) - k) by A2, RFINSEQ:def 1;

      1 <= (1 + k) & (k + 1) <= ( len g) by A2, NAT_1: 11, NAT_1: 13;

      then

       A6: (1 + k) in ( dom g) by FINSEQ_3: 25;

      

       A7: (( len g) - k) > 0 by A2, XREAL_1: 50;

      then (( len g) -' k) = (( len g) - k) by XREAL_0:def 2;

      then (( len g) - k) >= ( 0 + 1) by A7, NAT_1: 13;

      then 1 in ( dom (g /^ k)) by A5, FINSEQ_3: 25;

      

      hence ((g /^ k) . 1) = (g . (1 + k)) by A2, RFINSEQ:def 1

      .= (g /. (1 + k)) by A6, PARTFUN1:def 6;

      

       A8: (( len g) - k) > 0 by A2, XREAL_1: 50;

      then

       A9: (( len g) - k) = (( len g) -' k) by XREAL_0:def 2;

      then (( len g) -' k) >= ( 0 + 1) by A8, NAT_1: 13;

      then (( len g) -' k) in ( dom (g /^ k)) by A5, A9, FINSEQ_3: 25;

      

      hence ((g /^ k) . ( len (g /^ k))) = (g . ((( len g) -' k) + k)) by A2, A9, A3, RFINSEQ:def 1

      .= x2 by A1, A9;

    end;

    theorem :: FINTOPO6:54

    for g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT st g is_minimum_path_in (A,x1,x2) holds for k be Nat st 1 <= k & k <= ( len g) holds (g | k) is_minimum_path_in (A,x1,(g /. k))

    proof

      let g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT;

      assume

       A1: g is_minimum_path_in (A,x1,x2);

      then

       A2: ( rng g) c= A;

      

       A3: g is continuous by A1;

      then

       A4: 1 <= ( len g);

      

       A5: (g . ( len g)) = x2 by A1;

      let k be Nat;

      assume that

       A6: 1 <= k and

       A7: k <= ( len g);

      reconsider k as Element of NAT by ORDINAL1:def 12;

      

       A8: ((g | k) . 1) = x1 & ((g | k) . ( len (g | k))) = (g /. k) by A1, A6, A7, Th51;

      

       A9: (g | k) is continuous & ( rng (g | k)) c= A by A1, A6, A7, Th51;

      now

        per cases by A7, XXREAL_0: 1;

          suppose

           A10: k < ( len g);

          now

            k in ( dom g) by A6, A7, FINSEQ_3: 25;

            then

             A11: (g /. k) = (g . k) by PARTFUN1:def 6;

            (k + 1) <= ( len g) by A10, NAT_1: 13;

            then

             A12: ((g /^ k) . 1) = (g . (k + 1)) by FINSEQ_6: 114;

            ( rng (g /^ k)) c= ( rng g) by FINSEQ_5: 33;

            then

             A13: ( rng (g /^ k)) c= A by A2;

            assume not (g | k) is_minimum_path_in (A,x1,(g /. k));

            then

            consider h be FinSequence of FT such that

             A14: h is continuous and

             A15: ( rng h) c= A and

             A16: (h . 1) = x1 and

             A17: (h . ( len h)) = (g /. k) and

             A18: ( len (g | k)) > ( len h) by A9, A8;

            reconsider s = (h ^ (g /^ k)) as FinSequence of FT;

            

             A19: ( len s) = (( len h) + ( len (g /^ k))) by FINSEQ_1: 22;

            ( rng s) = (( rng h) \/ ( rng (g /^ k))) by FINSEQ_1: 31;

            then

             A20: ( rng s) c= A by A15, A13, XBOOLE_1: 8;

            

             A21: (g /^ k) is continuous by A1, A10, Th52;

            then 1 <= ( len (g /^ k));

            then ( len (g /^ k)) in ( dom (g /^ k)) by FINSEQ_3: 25;

            

            then

             A22: (s . ( len s)) = ((g /^ k) . ( len (g /^ k))) by A19, FINSEQ_1:def 7

            .= x2 by A5, A10, JORDAN4: 6;

            

             A23: 1 <= ( len h) by A14;

            then 1 in ( dom h) by FINSEQ_3: 25;

            then

             A24: (s . 1) = x1 by A16, FINSEQ_1:def 7;

            ( len h) in ( dom h) by A23, FINSEQ_3: 25;

            then (h . ( len h)) = (h /. ( len h)) by PARTFUN1:def 6;

            then ((g /^ k) . 1) in ( U_FT (h /. ( len h))) by A3, A6, A10, A17, A12, A11;

            then

             A25: s is continuous by A14, A21, Th44;

            g = ((g | k) ^ (g /^ k)) by RFINSEQ: 8;

            then ( len g) = (( len (g | k)) + ( len (g /^ k))) by FINSEQ_1: 22;

            then ( len s) < ( len g) by A18, A19, XREAL_1: 8;

            hence contradiction by A1, A25, A20, A24, A22;

          end;

          hence (g | k) is_minimum_path_in (A,x1,(g /. k));

        end;

          suppose

           A26: k = ( len g);

          

           A27: ( len g) in ( dom g) by A4, FINSEQ_3: 25;

          (g | k) = g by A26, FINSEQ_1: 58;

          hence (g | k) is_minimum_path_in (A,x1,(g /. k)) by A1, A26, A27, PARTFUN1:def 6;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO6:55

    for g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT st g is_minimum_path_in (A,x1,x2) holds g is one-to-one

    proof

      let g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT;

      assume

       A1: g is_minimum_path_in (A,x1,x2);

      then

       A2: g is continuous;

      

       A3: for h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = x2 holds ( len g) <= ( len h) by A1;

      

       A4: ( rng g) c= A by A1;

      

       A5: (g . 1) = x1 by A1;

      

       A6: (g . ( len g)) = x2 by A1;

      assume not g is one-to-one;

      then

      consider y1,y2 be object such that

       A7: y1 in ( dom g) and

       A8: y2 in ( dom g) and

       A9: (g . y1) = (g . y2) and

       A10: y1 <> y2 by FUNCT_1:def 4;

      reconsider n1 = y1, n2 = y2 as Element of NAT by A7, A8;

      

       A11: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

      then

       A12: 1 <= n1 by A7, FINSEQ_1: 1;

      

       A13: n2 <= ( len g) by A8, A11, FINSEQ_1: 1;

      

       A14: 1 <= n2 by A8, A11, FINSEQ_1: 1;

      

       A15: n1 <= ( len g) by A7, A11, FINSEQ_1: 1;

      per cases by A10, XXREAL_0: 1;

        suppose

         A16: n1 > n2;

        set k = (( len g) -' n1);

        set g2 = ((g | n2) ^ (g /^ n1));

        

         A17: ( len (g /^ n1)) = (( len g) - n1) by A15, RFINSEQ:def 1;

        

         A18: (( len g) - n1) >= 0 by A15, XREAL_1: 48;

        then

         A19: (( len g) -' n1) = (( len g) - n1) by XREAL_0:def 2;

        

         A20: ( len (g | n2)) = n2 by A13, FINSEQ_1: 59;

        

        then

         A21: (g2 . 1) = ((g | n2) . 1) by A14, FINSEQ_1: 64

        .= (g . 1) by A14, FINSEQ_3: 112;

        

         A22: ( len g2) = (( len (g | n2)) + ( len (g /^ n1))) by FINSEQ_1: 22

        .= (n2 + (( len g) - n1)) by A15, A20, RFINSEQ:def 1;

        per cases by A15, XXREAL_0: 1;

          suppose n1 < ( len g);

          then (n1 + 1) <= ( len g) by NAT_1: 13;

          then

           A23: ((n1 + 1) - n1) <= (( len g) - n1) by XREAL_1: 13;

          then

           A24: ( 0 + 1) <= (n2 + (( len g) - n1)) by XREAL_1: 7;

          

           A25: g2 is continuous

          proof

            thus ( len g2) >= 1 by A22, A24;

            let i be Nat, z1 be Element of FT;

            assume that

             A26: 1 <= i and

             A27: i < ( len g2) and

             A28: z1 = (g2 . i);

            

             A29: (i + 1) <= ( len g2) by A27, NAT_1: 13;

            reconsider i as Element of NAT by ORDINAL1:def 12;

            1 < (i + 1) by A26, NAT_1: 13;

            then (i + 1) in ( dom g2) by A29, FINSEQ_3: 25;

            then (g2 . (i + 1)) = (g2 /. (i + 1)) by PARTFUN1:def 6;

            then

            reconsider z2 = (g2 . (i + 1)) as Element of FT;

            now

              per cases ;

                suppose

                 A30: i < n2;

                then

                 A31: (i + 1) <= n2 by NAT_1: 13;

                (i + 1) <= ( len (g | n2)) by A20, A30, NAT_1: 13;

                

                then

                 A32: z2 = ((g | n2) . (i + 1)) by FINSEQ_1: 64, NAT_1: 12

                .= (g . (i + 1)) by A31, FINSEQ_3: 112;

                

                 A33: i < ( len g) by A13, A30, XXREAL_0: 2;

                z1 = ((g | n2) . i) by A20, A26, A28, A30, FINSEQ_1: 64

                .= (g . i) by A30, FINSEQ_3: 112;

                hence z2 in ( U_FT z1) by A2, A26, A33, A32;

              end;

                suppose

                 A34: i >= n2;

                (i - n2) < ((n2 + (( len g) - n1)) - n2) by A22, A27, XREAL_1: 9;

                then

                 A35: (i -' n2) < (( len g) - n1) by A34, XREAL_1: 233;

                then

                 A36: ((i -' n2) + n1) < ((( len g) - n1) + n1) by XREAL_1: 6;

                

                 A37: (( len (g | n2)) + (i -' n2)) = (n2 + (i - n2)) by A20, A34, XREAL_1: 233

                .= i;

                 A38:

                now

                  per cases by A34, XXREAL_0: 1;

                    suppose i > n2;

                    then

                     A39: (i - n2) > 0 by XREAL_1: 50;

                    then (i -' n2) = (i - n2) by XREAL_0:def 2;

                    then

                     A40: ( 0 + 1) <= (i -' n2) by A39, NAT_1: 13;

                    then

                     A41: (i -' n2) in ( dom (g /^ n1)) by A17, A35, FINSEQ_3: 25;

                    

                    thus z1 = ((g /^ n1) . (i -' n2)) by A17, A28, A35, A37, A40, FINSEQ_1: 65

                    .= (g . ((i -' n2) + n1)) by A15, A41, RFINSEQ:def 1;

                  end;

                    suppose

                     A42: i = n2;

                    

                    hence z1 = ((g | n2) . n2) by A20, A26, A28, FINSEQ_1: 64

                    .= (g . ( 0 + n1)) by A9, FINSEQ_3: 112

                    .= (g . ((i -' n2) + n1)) by A42, XREAL_1: 232;

                  end;

                end;

                (i -' n2) < (( len g) -' n1) by A15, A35, XREAL_1: 233;

                then ((i -' n2) + 1) <= (( len g) -' n1) by NAT_1: 13;

                then

                 A43: ((i -' n2) + 1) <= ( len (g /^ n1)) by A15, A17, XREAL_1: 233;

                1 <= ((i -' n2) + 1) by NAT_1: 12;

                then

                 A44: ((i -' n2) + 1) in ( dom (g /^ n1)) by A43, FINSEQ_3: 25;

                (( len (g | n2)) + ((i -' n2) + 1)) = (((i - n2) + 1) + n2) by A20, A34, XREAL_1: 233

                .= (i + 1);

                

                then

                 A45: z2 = ((g /^ n1) . ((i -' n2) + 1)) by A43, FINSEQ_1: 65, NAT_1: 12

                .= (g . (((i -' n2) + 1) + n1)) by A15, A44, RFINSEQ:def 1

                .= (g . (((i -' n2) + n1) + 1));

                1 <= ((i -' n2) + n1) by A12, NAT_1: 12;

                hence z2 in ( U_FT z1) by A2, A38, A45, A36;

              end;

            end;

            hence thesis;

          end;

          

           A46: ( rng (g /^ n1)) c= ( rng g) by FINSEQ_5: 33;

          ( rng g2) = (( rng (g | n2)) \/ ( rng (g /^ n1))) & ( rng (g | n2)) c= ( rng g) by FINSEQ_1: 31, FINSEQ_5: 19;

          then

           A47: ( rng g2) c= ( rng g) by A46, XBOOLE_1: 8;

          

           A48: (k + n1) = ( len g) by A19;

          

           A49: k in ( dom (g /^ n1)) by A19, A17, A23, FINSEQ_3: 25;

          

          then (g2 . (( len (g | n2)) + k)) = ((g /^ n1) . k) by FINSEQ_1:def 7

          .= x2 by A6, A15, A49, A48, RFINSEQ:def 1;

          then (g2 . ( len g2)) = x2 by A20, A22, A18, XREAL_0:def 2;

          then ( len g) <= ( len g2) by A4, A5, A3, A21, A47, A25, XBOOLE_1: 1;

          then (( len g) - n2) <= ((n2 + (( len g) - n1)) - n2) by A22, XREAL_1: 13;

          hence contradiction by A16, XREAL_1: 10;

        end;

          suppose

           A50: n1 = ( len g);

          

           A51: ( len (g /^ n1)) = (( len g) - n1) by A15, RFINSEQ:def 1;

          

           A52: g2 is continuous

          proof

            thus 1 <= ( len g2) by A8, A11, A22, A50, FINSEQ_1: 1;

            let i be Nat, z1 be Element of FT;

            assume that

             A53: 1 <= i and

             A54: i < ( len g2) and

             A55: z1 = (g2 . i);

            

             A56: (i + 1) <= ( len g2) by A54, NAT_1: 13;

            reconsider i as Element of NAT by ORDINAL1:def 12;

            1 < (i + 1) by A53, NAT_1: 13;

            then (i + 1) in ( dom g2) by A56, FINSEQ_3: 25;

            then (g2 . (i + 1)) = (g2 /. (i + 1)) by PARTFUN1:def 6;

            then

            reconsider z2 = (g2 . (i + 1)) as Element of FT;

            per cases ;

              suppose

               A57: i < n2;

              then

               A58: (i + 1) <= n2 by NAT_1: 13;

              (i + 1) <= ( len (g | n2)) by A20, A57, NAT_1: 13;

              

              then

               A59: z2 = ((g | n2) . (i + 1)) by FINSEQ_1: 64, NAT_1: 12

              .= (g . (i + 1)) by A58, FINSEQ_3: 112;

              

               A60: i < ( len g) by A13, A57, XXREAL_0: 2;

              z1 = ((g | n2) . i) by A20, A53, A55, A57, FINSEQ_1: 64

              .= (g . i) by A57, FINSEQ_3: 112;

              hence thesis by A2, A53, A60, A59;

            end;

              suppose

               A61: i >= n2;

              (i - n2) < ((n2 + (( len g) - n1)) - n2) by A22, A54, XREAL_1: 9;

              then

               A62: (i -' n2) < (( len g) - n1) by A61, XREAL_1: 233;

              then

               A63: ((i -' n2) + n1) < ((( len g) - n1) + n1) by XREAL_1: 6;

              

               A64: (( len (g | n2)) + (i -' n2)) = (n2 + (i - n2)) by A20, A61, XREAL_1: 233

              .= i;

               A65:

              now

                per cases by A61, XXREAL_0: 1;

                  suppose i > n2;

                  then

                   A66: (i - n2) > 0 by XREAL_1: 50;

                  then (i -' n2) = (i - n2) by XREAL_0:def 2;

                  then

                   A67: ( 0 + 1) <= (i -' n2) by A66, NAT_1: 13;

                  then

                   A68: (i -' n2) in ( dom (g /^ n1)) by A51, A62, FINSEQ_3: 25;

                  

                  thus z1 = ((g /^ n1) . (i -' n2)) by A51, A55, A62, A64, A67, FINSEQ_1: 65

                  .= (g . ((i -' n2) + n1)) by A15, A68, RFINSEQ:def 1;

                end;

                  suppose

                   A69: i = n2;

                  

                  hence z1 = ((g | n2) . n2) by A20, A53, A55, FINSEQ_1: 64

                  .= (g . ( 0 + n1)) by A9, FINSEQ_3: 112

                  .= (g . ((i -' n2) + n1)) by A69, XREAL_1: 232;

                end;

              end;

              (i -' n2) < (( len g) -' n1) by A15, A62, XREAL_1: 233;

              then ((i -' n2) + 1) <= (( len g) -' n1) by NAT_1: 13;

              then

               A70: ((i -' n2) + 1) <= ( len (g /^ n1)) by A15, A51, XREAL_1: 233;

              1 <= ((i -' n2) + 1) by NAT_1: 12;

              then

               A71: ((i -' n2) + 1) in ( dom (g /^ n1)) by A70, FINSEQ_3: 25;

              (( len (g | n2)) + ((i -' n2) + 1)) = (((i - n2) + 1) + n2) by A20, A61, XREAL_1: 233

              .= (i + 1);

              

              then

               A72: z2 = ((g /^ n1) . ((i -' n2) + 1)) by A70, FINSEQ_1: 65, NAT_1: 12

              .= (g . (((i -' n2) + 1) + n1)) by A15, A71, RFINSEQ:def 1

              .= (g . (((i -' n2) + n1) + 1));

              1 <= ((i -' n2) + n1) by A12, NAT_1: 12;

              hence thesis by A2, A65, A72, A63;

            end;

          end;

          

           A73: ( rng (g | n2)) c= ( rng g) by FINSEQ_5: 19;

          

           A74: g2 = ((g | n2) ^ {} ) by A50, FINSEQ_6: 167

          .= (g | n2) by FINSEQ_1: 34;

          then (g2 . ( len g2)) = x2 by A6, A9, A20, A50, FINSEQ_3: 112;

          then ( len g) <= ( len g2) by A4, A5, A3, A21, A74, A73, A52, XBOOLE_1: 1;

          then (( len g) - n2) <= ((n2 + (( len g) - n1)) - n2) by A22, XREAL_1: 13;

          hence contradiction by A16, XREAL_1: 10;

        end;

      end;

        suppose

         A75: n2 > n1;

        set k = (( len g) -' n2);

        set g2 = ((g | n1) ^ (g /^ n2));

        

         A76: ( len (g /^ n2)) = (( len g) - n2) by A13, RFINSEQ:def 1;

        (( len g) - n2) >= 0 by A13, XREAL_1: 48;

        then

         A77: (( len g) -' n2) = (( len g) - n2) by XREAL_0:def 2;

        

         A78: ( len (g | n1)) = n1 by A15, FINSEQ_1: 59;

        

        then

         A79: (g2 . 1) = ((g | n1) . 1) by A12, FINSEQ_1: 64

        .= x1 by A5, A12, FINSEQ_3: 112;

        

         A80: ( len g2) = (( len (g | n1)) + ( len (g /^ n2))) by FINSEQ_1: 22

        .= (n1 + (( len g) - n2)) by A13, A78, RFINSEQ:def 1;

        per cases by A13, XXREAL_0: 1;

          suppose n2 < ( len g);

          then (n2 + 1) <= ( len g) by NAT_1: 13;

          then

           A81: ((n2 + 1) - n2) <= (( len g) - n2) by XREAL_1: 13;

          then

           A82: ( 0 + 1) <= (n1 + (( len g) - n2)) by XREAL_1: 7;

          

           A83: g2 is continuous

          proof

            thus ( len g2) >= 1 by A80, A82;

            let i be Nat, z1 be Element of FT;

            assume that

             A84: 1 <= i and

             A85: i < ( len g2) and

             A86: z1 = (g2 . i);

            

             A87: (i + 1) <= ( len g2) by A85, NAT_1: 13;

            reconsider i as Element of NAT by ORDINAL1:def 12;

            1 < (i + 1) by A84, NAT_1: 13;

            then (i + 1) in ( dom g2) by A87, FINSEQ_3: 25;

            then (g2 . (i + 1)) = (g2 /. (i + 1)) by PARTFUN1:def 6;

            then

            reconsider z2 = (g2 . (i + 1)) as Element of FT;

            per cases ;

              suppose

               A88: i < n1;

              then

               A89: (i + 1) <= n1 by NAT_1: 13;

              (i + 1) <= ( len (g | n1)) by A78, A88, NAT_1: 13;

              

              then

               A90: z2 = ((g | n1) . (i + 1)) by FINSEQ_1: 64, NAT_1: 12

              .= (g . (i + 1)) by A89, FINSEQ_3: 112;

              

               A91: i < ( len g) by A15, A88, XXREAL_0: 2;

              z1 = ((g | n1) . i) by A78, A84, A86, A88, FINSEQ_1: 64

              .= (g . i) by A88, FINSEQ_3: 112;

              hence thesis by A2, A84, A91, A90;

            end;

              suppose

               A92: i >= n1;

              (i - n1) < ((n1 + (( len g) - n2)) - n1) by A80, A85, XREAL_1: 9;

              then

               A93: (i -' n1) < (( len g) - n2) by A92, XREAL_1: 233;

              then

               A94: ((i -' n1) + n2) < ((( len g) - n2) + n2) by XREAL_1: 6;

              

               A95: (( len (g | n1)) + (i -' n1)) = (n1 + (i - n1)) by A78, A92, XREAL_1: 233

              .= i;

               A96:

              now

                per cases by A92, XXREAL_0: 1;

                  suppose i > n1;

                  then

                   A97: (i - n1) > 0 by XREAL_1: 50;

                  then (i -' n1) = (i - n1) by XREAL_0:def 2;

                  then

                   A98: ( 0 + 1) <= (i -' n1) by A97, NAT_1: 13;

                  then

                   A99: (i -' n1) in ( dom (g /^ n2)) by A76, A93, FINSEQ_3: 25;

                  

                  thus z1 = ((g /^ n2) . (i -' n1)) by A76, A86, A93, A95, A98, FINSEQ_1: 65

                  .= (g . ((i -' n1) + n2)) by A13, A99, RFINSEQ:def 1;

                end;

                  suppose

                   A100: i = n1;

                  

                  hence z1 = ((g | n1) . n1) by A78, A84, A86, FINSEQ_1: 64

                  .= (g . ( 0 + n2)) by A9, FINSEQ_3: 112

                  .= (g . ((i -' n1) + n2)) by A100, XREAL_1: 232;

                end;

              end;

              (i -' n1) < (( len g) -' n2) by A13, A93, XREAL_1: 233;

              then ((i -' n1) + 1) <= (( len g) -' n2) by NAT_1: 13;

              then

               A101: ((i -' n1) + 1) <= ( len (g /^ n2)) by A13, A76, XREAL_1: 233;

              1 <= ((i -' n1) + 1) by NAT_1: 12;

              then

               A102: ((i -' n1) + 1) in ( dom (g /^ n2)) by A101, FINSEQ_3: 25;

              (( len (g | n1)) + ((i -' n1) + 1)) = (((i - n1) + 1) + n1) by A78, A92, XREAL_1: 233

              .= (i + 1);

              

              then

               A103: z2 = ((g /^ n2) . ((i -' n1) + 1)) by A101, FINSEQ_1: 65, NAT_1: 12

              .= (g . (((i -' n1) + 1) + n2)) by A13, A102, RFINSEQ:def 1

              .= (g . (((i -' n1) + n2) + 1));

              1 <= ((i -' n1) + n2) by A14, NAT_1: 12;

              hence thesis by A2, A96, A103, A94;

            end;

          end;

          

           A104: ( rng (g /^ n2)) c= ( rng g) by FINSEQ_5: 33;

          ( rng g2) = (( rng (g | n1)) \/ ( rng (g /^ n2))) & ( rng (g | n1)) c= ( rng g) by FINSEQ_1: 31, FINSEQ_5: 19;

          then ( rng g2) c= ( rng g) by A104, XBOOLE_1: 8;

          then

           A105: ( rng g2) c= A by A4;

          

           A106: (k + n2) = ( len g) by A77;

          

           A107: k in ( dom (g /^ n2)) by A77, A76, A81, FINSEQ_3: 25;

          

          then (g2 . (( len (g | n1)) + k)) = ((g /^ n2) . k) by FINSEQ_1:def 7

          .= x2 by A6, A13, A107, A106, RFINSEQ:def 1;

          then (g2 . ( len g2)) = x2 by A15, A80, A77, FINSEQ_1: 59;

          then ( len g) <= ( len g2) by A1, A79, A105, A83;

          then (( len g) - n1) <= ((n1 + (( len g) - n2)) - n1) by A80, XREAL_1: 13;

          hence contradiction by A75, XREAL_1: 10;

        end;

          suppose

           A108: n2 = ( len g);

          

           A109: ( len (g /^ n2)) = (( len g) - n2) by A13, RFINSEQ:def 1;

          

           A110: g2 is continuous

          proof

            thus ( len g2) >= 1 by A7, A11, A80, A108, FINSEQ_1: 1;

            let i be Nat, z1 be Element of FT;

            assume that

             A111: 1 <= i and

             A112: i < ( len g2) and

             A113: z1 = (g2 . i);

            

             A114: (i + 1) <= ( len g2) by A112, NAT_1: 13;

            reconsider i as Element of NAT by ORDINAL1:def 12;

            1 < (i + 1) by A111, NAT_1: 13;

            then (i + 1) in ( dom g2) by A114, FINSEQ_3: 25;

            then (g2 . (i + 1)) = (g2 /. (i + 1)) by PARTFUN1:def 6;

            then

            reconsider z2 = (g2 . (i + 1)) as Element of FT;

            per cases ;

              suppose

               A115: i < n1;

              then

               A116: (i + 1) <= n1 by NAT_1: 13;

              (i + 1) <= ( len (g | n1)) by A78, A115, NAT_1: 13;

              

              then

               A117: z2 = ((g | n1) . (i + 1)) by FINSEQ_1: 64, NAT_1: 12

              .= (g . (i + 1)) by A116, FINSEQ_3: 112;

              

               A118: i < ( len g) by A15, A115, XXREAL_0: 2;

              z1 = ((g | n1) . i) by A78, A111, A113, A115, FINSEQ_1: 64

              .= (g . i) by A115, FINSEQ_3: 112;

              hence thesis by A2, A111, A118, A117;

            end;

              suppose

               A119: i >= n1;

              (i - n1) < ((n1 + (( len g) - n2)) - n1) by A80, A112, XREAL_1: 9;

              then

               A120: (i -' n1) < (( len g) - n2) by A119, XREAL_1: 233;

              then

               A121: ((i -' n1) + n2) < ((( len g) - n2) + n2) by XREAL_1: 6;

              

               A122: (( len (g | n1)) + (i -' n1)) = (n1 + (i - n1)) by A78, A119, XREAL_1: 233

              .= i;

               A123:

              now

                per cases by A119, XXREAL_0: 1;

                  suppose i > n1;

                  then

                   A124: (i - n1) > 0 by XREAL_1: 50;

                  then (i -' n1) = (i - n1) by XREAL_0:def 2;

                  then

                   A125: ( 0 + 1) <= (i -' n1) by A124, NAT_1: 13;

                  then

                   A126: (i -' n1) in ( dom (g /^ n2)) by A109, A120, FINSEQ_3: 25;

                  

                  thus z1 = ((g /^ n2) . (i -' n1)) by A109, A113, A120, A122, A125, FINSEQ_1: 65

                  .= (g . ((i -' n1) + n2)) by A13, A126, RFINSEQ:def 1;

                end;

                  suppose

                   A127: i = n1;

                  

                  hence z1 = ((g | n1) . n1) by A78, A111, A113, FINSEQ_1: 64

                  .= (g . ( 0 + n2)) by A9, FINSEQ_3: 112

                  .= (g . ((i -' n1) + n2)) by A127, XREAL_1: 232;

                end;

              end;

              (i -' n1) < (( len g) -' n2) by A13, A120, XREAL_1: 233;

              then ((i -' n1) + 1) <= (( len g) -' n2) by NAT_1: 13;

              then

               A128: ((i -' n1) + 1) <= ( len (g /^ n2)) by A13, A109, XREAL_1: 233;

              1 <= ((i -' n1) + 1) by NAT_1: 12;

              then

               A129: ((i -' n1) + 1) in ( dom (g /^ n2)) by A128, FINSEQ_3: 25;

              (( len (g | n1)) + ((i -' n1) + 1)) = (((i - n1) + 1) + n1) by A78, A119, XREAL_1: 233

              .= (i + 1);

              

              then

               A130: z2 = ((g /^ n2) . ((i -' n1) + 1)) by A128, FINSEQ_1: 65, NAT_1: 12

              .= (g . (((i -' n1) + 1) + n2)) by A13, A129, RFINSEQ:def 1

              .= (g . (((i -' n1) + n2) + 1));

              1 <= ((i -' n1) + n2) by A14, NAT_1: 12;

              hence thesis by A2, A123, A130, A121;

            end;

          end;

          

           A131: g2 = ((g | n1) ^ {} ) by A108, FINSEQ_6: 167

          .= (g | n1) by FINSEQ_1: 34;

          ( rng (g | n1)) c= ( rng g) by FINSEQ_5: 19;

          then

           A132: ( rng g2) c= A by A4, A131;

          (g2 . ( len g2)) = x2 by A6, A9, A78, A108, A131, FINSEQ_3: 112;

          then ( len g) <= ( len g2) by A1, A79, A132, A110;

          then (( len g) - n1) <= ((n1 + (( len g) - n2)) - n1) by A80, XREAL_1: 13;

          hence contradiction by A75, XREAL_1: 10;

        end;

      end;

    end;

    definition

      let FT;

      let f be FinSequence of FT;

      :: FINTOPO6:def9

      attr f is inv_continuous means 1 <= ( len f) & for i,j be Nat, y be Element of FT st 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) & y = (f . i) & i <> j & (f . j) in ( U_FT y) holds i = (j + 1) or j = (i + 1);

    end

    theorem :: FINTOPO6:56

    

     Th55: for g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT st g is_minimum_path_in (A,x1,x2) & FT is symmetric holds g is inv_continuous

    proof

      let g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT;

      assume that

       A1: g is_minimum_path_in (A,x1,x2) and

       A2: FT is symmetric;

      

       A3: (g . 1) = x1 by A1;

      

       A4: (g . ( len g)) = x2 by A1;

      

       A5: g is continuous by A1;

      hence 1 <= ( len g);

      let i2,j2 be Nat, y be Element of FT;

      assume that

       A6: 1 <= i2 and

       A7: i2 <= ( len g) and

       A8: 1 <= j2 and

       A9: j2 <= ( len g) and

       A10: y = (g . i2) and

       A11: i2 <> j2 and

       A12: (g . j2) in ( U_FT y);

      

       A13: ( rng g) c= A by A1;

      hereby

        assume that

         A14: i2 <> (j2 + 1) and

         A15: j2 <> (i2 + 1);

        per cases by A11, XXREAL_0: 1;

          suppose

           A16: i2 < j2;

          set n1 = (j2 -' 1), n2 = i2;

          reconsider n1, n2 as Element of NAT by ORDINAL1:def 12;

          (i2 + 1) <= j2 by A16, NAT_1: 13;

          then (i2 + 1) < j2 by A15, XXREAL_0: 1;

          then i2 < (j2 - 1) by XREAL_1: 20;

          then

           A17: n1 > n2 by A8, XREAL_1: 233;

          1 < j2 by A6, A16, XXREAL_0: 2;

          then (1 + 1) <= j2 by NAT_1: 13;

          then 1 <= (j2 - 1) by XREAL_1: 19;

          then

           A18: 1 <= n1 by A8, XREAL_1: 233;

          set k = (( len g) -' n1);

          reconsider g2 = ((g | n2) ^ (g /^ n1)) as FinSequence of FT;

          

           A19: ( len (g | n2)) = n2 by A7, FINSEQ_1: 59;

          

           A20: (j2 -' 1) <= j2 by NAT_D: 35;

          then

           A21: n1 <= ( len g) by A9, XXREAL_0: 2;

          then

           A22: ( len (g /^ n1)) = (( len g) - n1) by RFINSEQ:def 1;

          

           A23: (( len g) - n1) >= 0 by A21, XREAL_1: 48;

          then

           A24: (( len g) -' n1) = (( len g) - n1) by XREAL_0:def 2;

          

           A25: ( len g2) = (( len (g | n2)) + ( len (g /^ n1))) by FINSEQ_1: 22

          .= (n2 + (( len g) - n1)) by A21, A19, RFINSEQ:def 1;

          

           A26: (g2 . 1) = ((g | n2) . 1) by A6, A19, FINSEQ_1: 64

          .= x1 by A3, A6, FINSEQ_3: 112;

          now

            per cases by A21, XXREAL_0: 1;

              suppose n1 < ( len g);

              then (n1 + 1) <= ( len g) by NAT_1: 13;

              then

               A27: ((n1 + 1) - n1) <= (( len g) - n1) by XREAL_1: 13;

              then

               A28: ( 0 + 1) <= (n2 + (( len g) - n1)) by XREAL_1: 7;

              

               A29: g2 is continuous

              proof

                thus ( len g2) >= 1 by A25, A28;

                let i be Nat, z1 be Element of FT;

                assume that

                 A30: 1 <= i and

                 A31: i < ( len g2) and

                 A32: z1 = (g2 . i);

                

                 A33: (i + 1) <= ( len g2) by A31, NAT_1: 13;

                reconsider i as Element of NAT by ORDINAL1:def 12;

                1 < (i + 1) by A30, NAT_1: 13;

                then (i + 1) in ( dom g2) by A33, FINSEQ_3: 25;

                then (g2 . (i + 1)) = (g2 /. (i + 1)) by PARTFUN1:def 6;

                then

                reconsider z2 = (g2 . (i + 1)) as Element of FT;

                per cases ;

                  suppose

                   A34: i < n2;

                  then

                   A35: (i + 1) <= n2 by NAT_1: 13;

                  (i + 1) <= ( len (g | n2)) by A19, A34, NAT_1: 13;

                  

                  then

                   A36: z2 = ((g | n2) . (i + 1)) by FINSEQ_1: 64, NAT_1: 12

                  .= (g . (i + 1)) by A35, FINSEQ_3: 112;

                  

                   A37: i < ( len g) by A7, A34, XXREAL_0: 2;

                  z1 = ((g | n2) . i) by A19, A30, A32, A34, FINSEQ_1: 64

                  .= (g . i) by A34, FINSEQ_3: 112;

                  hence thesis by A5, A30, A37, A36;

                end;

                  suppose

                   A38: i >= n2;

                  (i - n2) < ((n2 + (( len g) - n1)) - n2) by A25, A31, XREAL_1: 9;

                  then

                   A39: (i -' n2) < (( len g) - n1) by A38, XREAL_1: 233;

                  then (i -' n2) < (( len g) -' n1) by A9, A20, XREAL_1: 233, XXREAL_0: 2;

                  then ((i -' n2) + 1) <= (( len g) -' n1) by NAT_1: 13;

                  then

                   A40: ((i -' n2) + 1) <= ( len (g /^ n1)) by A9, A20, A22, XREAL_1: 233, XXREAL_0: 2;

                  

                   A41: (( len (g | n2)) + (i -' n2)) = (n2 + (i - n2)) by A19, A38, XREAL_1: 233

                  .= i;

                  

                   A42: (( len (g | n2)) + ((i -' n2) + 1)) = (((i - n2) + 1) + n2) by A19, A38, XREAL_1: 233

                  .= (i + 1);

                  1 <= ((i -' n2) + 1) by NAT_1: 12;

                  then

                   A43: ((i -' n2) + 1) in ( dom (g /^ n1)) by A40, FINSEQ_3: 25;

                  per cases by A38, XXREAL_0: 1;

                    suppose i > n2;

                    then

                     A44: (i - n2) > 0 by XREAL_1: 50;

                    then (i -' n2) = (i - n2) by XREAL_0:def 2;

                    then

                     A45: ( 0 + 1) <= (i -' n2) by A44, NAT_1: 13;

                    then

                     A46: (i -' n2) in ( dom (g /^ n1)) by A22, A39, FINSEQ_3: 25;

                    

                     A47: z2 = ((g /^ n1) . ((i -' n2) + 1)) by A40, A42, FINSEQ_1: 65, NAT_1: 12

                    .= (g . (((i -' n2) + 1) + n1)) by A21, A43, RFINSEQ:def 1

                    .= (g . (((i -' n2) + n1) + 1));

                    

                     A48: 1 <= ((i -' n2) + n1) & ((i -' n2) + n1) < ((( len g) - n1) + n1) by A18, A39, NAT_1: 12, XREAL_1: 6;

                    z1 = ((g /^ n1) . (i -' n2)) by A22, A32, A39, A41, A45, FINSEQ_1: 65

                    .= (g . ((i -' n2) + n1)) by A21, A46, RFINSEQ:def 1;

                    hence thesis by A5, A47, A48;

                  end;

                    suppose

                     A49: i = n2;

                    

                    then

                     A50: z1 = ((g | n2) . n2) by A19, A30, A32, FINSEQ_1: 64

                    .= y by A10, FINSEQ_3: 112;

                    z2 = ((g /^ n1) . ((i -' n2) + 1)) by A40, A42, FINSEQ_1: 65, NAT_1: 12

                    .= (g . (((i -' n2) + 1) + n1)) by A21, A43, RFINSEQ:def 1

                    .= (g . (((i -' n2) + n1) + 1))

                    .= (g . (( 0 + (j2 -' 1)) + 1)) by A49, XREAL_1: 232

                    .= (g . ((j2 - 1) + 1)) by A8, XREAL_1: 233;

                    hence thesis by A12, A50;

                  end;

                end;

              end;

              

               A51: ( rng (g /^ n1)) c= ( rng g) by FINSEQ_5: 33;

              ( rng g2) = (( rng (g | n2)) \/ ( rng (g /^ n1))) & ( rng (g | n2)) c= ( rng g) by FINSEQ_1: 31, FINSEQ_5: 19;

              then ( rng g2) c= ( rng g) by A51, XBOOLE_1: 8;

              then

               A52: ( rng g2) c= A by A13;

              

               A53: (k + n1) = ( len g) by A24;

              

               A54: k in ( dom (g /^ n1)) by A24, A22, A27, FINSEQ_3: 25;

              

              then (g2 . (( len (g | n2)) + k)) = ((g /^ n1) . k) by FINSEQ_1:def 7

              .= x2 by A4, A21, A54, A53, RFINSEQ:def 1;

              then (g2 . ( len g2)) = x2 by A19, A25, A23, XREAL_0:def 2;

              then ( len g) <= ( len g2) by A1, A26, A52, A29;

              then (( len g) - n2) <= ((n2 + (( len g) - n1)) - n2) by A25, XREAL_1: 13;

              hence contradiction by A17, XREAL_1: 10;

            end;

              suppose n1 = ( len g);

              then (j2 - 1) = ( len g) by A8, XREAL_1: 233;

              then j2 = (( len g) + 1);

              hence contradiction by A9, NAT_1: 13;

            end;

          end;

          hence contradiction;

        end;

          suppose

           A55: j2 < i2;

          reconsider n1 = (i2 -' 1), n2 = j2 as Element of NAT by ORDINAL1:def 12;

          (j2 + 1) <= i2 by A55, NAT_1: 13;

          then (j2 + 1) < i2 by A14, XXREAL_0: 1;

          then j2 < (i2 - 1) by XREAL_1: 20;

          then

           A56: n1 > n2 by A6, XREAL_1: 233;

          1 < i2 by A8, A55, XXREAL_0: 2;

          then (1 + 1) <= i2 by NAT_1: 13;

          then 1 <= (i2 - 1) by XREAL_1: 19;

          then

           A57: 1 <= n1 by A6, XREAL_1: 233;

          set k = (( len g) -' n1);

          reconsider g2 = ((g | n2) ^ (g /^ n1)) as FinSequence of FT;

          

           A58: ( len (g | n2)) = n2 by A9, FINSEQ_1: 59;

          

           A59: (i2 -' 1) <= i2 by NAT_D: 35;

          then

           A60: n1 <= ( len g) by A7, XXREAL_0: 2;

          then

           A61: ( len (g /^ n1)) = (( len g) - n1) by RFINSEQ:def 1;

          

           A62: (( len g) - n1) >= 0 by A60, XREAL_1: 48;

          then

           A63: (( len g) -' n1) = (( len g) - n1) by XREAL_0:def 2;

          

           A64: ( len g2) = (( len (g | n2)) + ( len (g /^ n1))) by FINSEQ_1: 22

          .= (n2 + (( len g) - n1)) by A60, A58, RFINSEQ:def 1;

          

           A65: (g2 . 1) = ((g | n2) . 1) by A8, A58, FINSEQ_1: 64

          .= x1 by A3, A8, FINSEQ_3: 112;

          now

            per cases by A60, XXREAL_0: 1;

              suppose n1 < ( len g);

              then (n1 + 1) <= ( len g) by NAT_1: 13;

              then

               A66: ((n1 + 1) - n1) <= (( len g) - n1) by XREAL_1: 13;

              then

               A67: ( 0 + 1) <= (n2 + (( len g) - n1)) by XREAL_1: 7;

              

               A68: g2 is continuous

              proof

                thus ( len g2) >= 1 by A64, A67;

                let i be Nat, z1 be Element of FT;

                assume that

                 A69: 1 <= i and

                 A70: i < ( len g2) and

                 A71: z1 = (g2 . i);

                

                 A72: (i + 1) <= ( len g2) by A70, NAT_1: 13;

                reconsider i as Element of NAT by ORDINAL1:def 12;

                1 < (i + 1) by A69, NAT_1: 13;

                then (i + 1) in ( dom g2) by A72, FINSEQ_3: 25;

                then (g2 . (i + 1)) = (g2 /. (i + 1)) by PARTFUN1:def 6;

                then

                reconsider z2 = (g2 . (i + 1)) as Element of FT;

                per cases ;

                  suppose

                   A73: i < n2;

                  then

                   A74: (i + 1) <= n2 by NAT_1: 13;

                  (i + 1) <= ( len (g | n2)) by A58, A73, NAT_1: 13;

                  

                  then

                   A75: z2 = ((g | n2) . (i + 1)) by FINSEQ_1: 64, NAT_1: 12

                  .= (g . (i + 1)) by A74, FINSEQ_3: 112;

                  

                   A76: i < ( len g) by A9, A73, XXREAL_0: 2;

                  z1 = ((g | n2) . i) by A58, A69, A71, A73, FINSEQ_1: 64

                  .= (g . i) by A73, FINSEQ_3: 112;

                  hence thesis by A5, A69, A76, A75;

                end;

                  suppose

                   A77: i >= n2;

                  (i - n2) < ((n2 + (( len g) - n1)) - n2) by A64, A70, XREAL_1: 9;

                  then

                   A78: (i -' n2) < (( len g) - n1) by A77, XREAL_1: 233;

                  then (i -' n2) < (( len g) -' n1) by A7, A59, XREAL_1: 233, XXREAL_0: 2;

                  then ((i -' n2) + 1) <= (( len g) -' n1) by NAT_1: 13;

                  then

                   A79: ((i -' n2) + 1) <= ( len (g /^ n1)) by A7, A59, A61, XREAL_1: 233, XXREAL_0: 2;

                  

                   A80: (( len (g | n2)) + (i -' n2)) = (n2 + (i - n2)) by A58, A77, XREAL_1: 233

                  .= i;

                  

                   A81: (( len (g | n2)) + ((i -' n2) + 1)) = (((i - n2) + 1) + n2) by A58, A77, XREAL_1: 233

                  .= (i + 1);

                  1 <= ((i -' n2) + 1) by NAT_1: 12;

                  then

                   A82: ((i -' n2) + 1) in ( dom (g /^ n1)) by A79, FINSEQ_3: 25;

                  per cases by A77, XXREAL_0: 1;

                    suppose i > n2;

                    then

                     A83: (i - n2) > 0 by XREAL_1: 50;

                    then (i -' n2) = (i - n2) by XREAL_0:def 2;

                    then

                     A84: ( 0 + 1) <= (i -' n2) by A83, NAT_1: 13;

                    then

                     A85: (i -' n2) in ( dom (g /^ n1)) by A61, A78, FINSEQ_3: 25;

                    

                     A86: z2 = ((g /^ n1) . ((i -' n2) + 1)) by A79, A81, FINSEQ_1: 65, NAT_1: 12

                    .= (g . (((i -' n2) + 1) + n1)) by A60, A82, RFINSEQ:def 1

                    .= (g . (((i -' n2) + n1) + 1));

                    

                     A87: 1 <= ((i -' n2) + n1) & ((i -' n2) + n1) < ((( len g) - n1) + n1) by A57, A78, NAT_1: 12, XREAL_1: 6;

                    z1 = ((g /^ n1) . (i -' n2)) by A61, A71, A78, A80, A84, FINSEQ_1: 65

                    .= (g . ((i -' n2) + n1)) by A60, A85, RFINSEQ:def 1;

                    hence thesis by A5, A86, A87;

                  end;

                    suppose

                     A88: i = n2;

                    

                    then

                     A89: z1 = ((g | n2) . n2) by A58, A69, A71, FINSEQ_1: 64

                    .= (g . j2) by FINSEQ_3: 112;

                    z2 = ((g /^ n1) . ((i -' n2) + 1)) by A79, A81, FINSEQ_1: 65, NAT_1: 12

                    .= (g . (((i -' n2) + 1) + n1)) by A60, A82, RFINSEQ:def 1

                    .= (g . (((i -' n2) + n1) + 1))

                    .= (g . (( 0 + (i2 -' 1)) + 1)) by A88, XREAL_1: 232

                    .= (g . ((i2 - 1) + 1)) by A6, XREAL_1: 233

                    .= y by A10;

                    hence thesis by A2, A12, A89;

                  end;

                end;

              end;

              

               A90: ( rng (g /^ n1)) c= ( rng g) by FINSEQ_5: 33;

              ( rng g2) = (( rng (g | n2)) \/ ( rng (g /^ n1))) & ( rng (g | n2)) c= ( rng g) by FINSEQ_1: 31, FINSEQ_5: 19;

              then ( rng g2) c= ( rng g) by A90, XBOOLE_1: 8;

              then

               A91: ( rng g2) c= A by A13;

              

               A92: (k + n1) = ( len g) by A63;

              

               A93: k in ( dom (g /^ n1)) by A63, A61, A66, FINSEQ_3: 25;

              

              then (g2 . (( len (g | n2)) + k)) = ((g /^ n1) . k) by FINSEQ_1:def 7

              .= x2 by A4, A60, A93, A92, RFINSEQ:def 1;

              then (g2 . ( len g2)) = x2 by A58, A64, A62, XREAL_0:def 2;

              then ( len g) <= ( len g2) by A1, A65, A91, A68;

              then (( len g) - n2) <= ((n2 + (( len g) - n1)) - n2) by A64, XREAL_1: 13;

              hence contradiction by A56, XREAL_1: 10;

            end;

              suppose n1 = ( len g);

              then (i2 - 1) = ( len g) by A6, XREAL_1: 233;

              then i2 = (( len g) + 1);

              hence contradiction by A7, NAT_1: 13;

            end;

          end;

          hence contradiction;

        end;

      end;

    end;

    theorem :: FINTOPO6:57

    for g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT st g is_minimum_path_in (A,x1,x2) & FT is filled symmetric & x1 <> x2 holds (for i be Nat st 1 < i & i < ( len g) holds (( rng g) /\ ( U_FT (g /. i))) = {(g . (i -' 1)), (g . i), (g . (i + 1))}) & (( rng g) /\ ( U_FT (g /. 1))) = {(g . 1), (g . 2)} & (( rng g) /\ ( U_FT (g /. ( len g)))) = {(g . (( len g) -' 1)), (g . ( len g))}

    proof

      let g be FinSequence of FT, A be Subset of FT, x1,x2 be Element of FT;

      assume that

       A1: g is_minimum_path_in (A,x1,x2) and

       A2: FT is filled symmetric and

       A3: x1 <> x2;

      

       A4: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

      

       A5: g is continuous by A1;

      then

       A6: 1 <= ( len g);

      then

       A7: ( len g) in ( dom g) by A4;

      then

       A8: (g . ( len g)) = (g /. ( len g)) by PARTFUN1:def 6;

      

       A9: g is inv_continuous by A1, A2, Th55;

      then

       A10: 1 <= ( len g);

      thus for i be Nat st 1 < i & i < ( len g) holds (( rng g) /\ ( U_FT (g /. i))) = {(g . (i -' 1)), (g . i), (g . (i + 1))}

      proof

        let i be Nat;

        assume that

         A11: 1 < i and

         A12: i < ( len g);

        

         A13: i in ( Seg ( len g)) by A11, A12;

        1 < (i + 1) & (i + 1) <= ( len g) by A11, A12, NAT_1: 13;

        then

         A14: (i + 1) in ( Seg ( len g));

        (i -' 1) <= i by NAT_D: 35;

        then

         A15: (i -' 1) < ( len g) by A12, XXREAL_0: 2;

        (1 + 1) <= i by A11, NAT_1: 13;

        then

         A16: 1 <= (i - 1) by XREAL_1: 19;

        then 1 <= (i -' 1) by A11, XREAL_1: 233;

        then

         A17: (i -' 1) in ( Seg ( len g)) by A15;

        

         A18: ((i -' 1) + 1) = ((i - 1) + 1) by A11, XREAL_1: 233

        .= i;

        thus (( rng g) /\ ( U_FT (g /. i))) = {(g . (i -' 1)), (g . i), (g . (i + 1))}

        proof

          thus (( rng g) /\ ( U_FT (g /. i))) c= {(g . (i -' 1)), (g . i), (g . (i + 1))}

          proof

            let x be object;

            assume

             A19: x in (( rng g) /\ ( U_FT (g /. i)));

            then

             A20: x in ( U_FT (g /. i)) by XBOOLE_0:def 4;

            x in ( rng g) by A19, XBOOLE_0:def 4;

            then

            consider nx be object such that

             A21: nx in ( dom g) and

             A22: x = (g . nx) by FUNCT_1:def 3;

            reconsider j = nx as Element of NAT by A21;

            i = (j + 1) implies (i - 1) = j;

            then

             A23: i = (j + 1) implies (i -' 1) = j by A11, XREAL_1: 233;

            

             A24: (g /. i) = (g . i) by A4, A13, PARTFUN1:def 6;

            1 <= j & j <= ( len g) by A4, A21, FINSEQ_1: 1;

            then j = i or i = (j + 1) or j = (i + 1) by A9, A11, A12, A20, A22, A24;

            hence thesis by A22, A23, ENUMSET1:def 1;

          end;

          let x be object;

          

           A25: (g . i) = (g /. i) by A4, A13, PARTFUN1:def 6;

          

           A26: (g . (i -' 1)) = (g /. (i -' 1)) by A4, A17, PARTFUN1:def 6;

          assume

           A27: x in {(g . (i -' 1)), (g . i), (g . (i + 1))};

          per cases by A27, ENUMSET1:def 1;

            suppose

             A28: x = (g . (i -' 1));

            (g . i) in ( U_FT (g /. (i -' 1))) by A5, A16, A15, A18, A26;

            then

             A29: x in ( U_FT (g /. i)) by A2, A25, A26, A28;

            x in ( rng g) by A4, A17, A28, FUNCT_1:def 3;

            hence thesis by A29, XBOOLE_0:def 4;

          end;

            suppose x = (g . i);

            then x in ( rng g) & x in ( U_FT (g /. i)) by A2, A4, A13, A25, FUNCT_1:def 3;

            hence thesis by XBOOLE_0:def 4;

          end;

            suppose x = (g . (i + 1));

            then x in ( rng g) & x in ( U_FT (g /. i)) by A5, A4, A11, A12, A14, A25, FUNCT_1:def 3;

            hence thesis by XBOOLE_0:def 4;

          end;

        end;

      end;

      (g . 1) = x1 & (g . ( len g)) = x2 by A1;

      then

       A30: 1 < ( len g) by A3, A6, XXREAL_0: 1;

      then

       A31: (1 + 1) <= ( len g) by NAT_1: 13;

      then

       A32: ((1 + 1) - 1) <= (( len g) - 1) by XREAL_1: 13;

      

       A33: 1 in ( dom g) by A10, FINSEQ_3: 25;

      then

       A34: (g . 1) = (g /. 1) by PARTFUN1:def 6;

      thus (( rng g) /\ ( U_FT (g /. 1))) = {(g . 1), (g . 2)}

      proof

        thus (( rng g) /\ ( U_FT (g /. 1))) c= {(g . 1), (g . 2)}

        proof

          let x be object;

          assume

           A35: x in (( rng g) /\ ( U_FT (g /. 1)));

          then

           A36: x in ( U_FT (g /. 1)) by XBOOLE_0:def 4;

          x in ( rng g) by A35, XBOOLE_0:def 4;

          then

          consider y be object such that

           A37: y in ( dom g) and

           A38: x = (g . y) by FUNCT_1:def 3;

          reconsider j = y as Element of NAT by A37;

          

           A39: 1 <= j by A4, A37, FINSEQ_1: 1;

          j <= ( len g) by A4, A37, FINSEQ_1: 1;

          then (1 + 1) = j or 1 = j or (j + 1) = 1 by A9, A34, A36, A38, A39;

          then (1 + 1) = j or 1 = j by A39, XREAL_1: 7;

          hence thesis by A38, TARSKI:def 2;

        end;

        let x be object;

        2 in ( dom g) by A31, A4;

        then

         A40: x = (g . 2) implies x in ( rng g) by FUNCT_1:def 3;

        assume

         A41: x in {(g . 1), (g . 2)};

         A42:

        now

          per cases by A41, TARSKI:def 2;

            case x = (g . 1);

            hence x in ( U_FT (g /. 1)) by A2, A34;

          end;

            case

             A43: x = (g . 2);

            then

            reconsider xx = x as Element of FT by A40;

            xx = (g . (1 + 1)) by A43;

            hence x in ( U_FT (g /. 1)) by A5, A30, A34;

          end;

        end;

        x = (g . 1) implies x in ( rng g) by A33, FUNCT_1:def 3;

        hence thesis by A40, A42, XBOOLE_0:def 4;

      end;

      ( len g) < (( len g) + 1) by NAT_1: 13;

      then

       A44: (( len g) - 1) < ((( len g) + 1) - 1) by XREAL_1: 14;

      then

       A45: (( len g) -' 1) < ( len g) by A10, XREAL_1: 233;

      

       A46: (( len g) -' 1) = (( len g) - 1) by A10, XREAL_1: 233;

      then

       A47: (( len g) -' 1) in ( dom g) by A32, A44, FINSEQ_3: 25;

      then

       A48: (g . (( len g) -' 1)) = (g /. (( len g) -' 1)) by PARTFUN1:def 6;

      

       A49: 1 <= (( len g) -' 1) by A10, A32, XREAL_1: 233;

      thus (( rng g) /\ ( U_FT (g /. ( len g)))) = {(g . (( len g) -' 1)), (g . ( len g))}

      proof

        thus (( rng g) /\ ( U_FT (g /. ( len g)))) c= {(g . (( len g) -' 1)), (g . ( len g))}

        proof

          let x be object;

          assume

           A50: x in (( rng g) /\ ( U_FT (g /. ( len g))));

          then

           A51: x in ( U_FT (g /. ( len g))) by XBOOLE_0:def 4;

          x in ( rng g) by A50, XBOOLE_0:def 4;

          then

          consider y be object such that

           A52: y in ( dom g) and

           A53: x = (g . y) by FUNCT_1:def 3;

          reconsider ny = y as Element of NAT by A52;

          

           A54: ny <= ( len g) by A4, A52, FINSEQ_1: 1;

          1 <= ny by A4, A52, FINSEQ_1: 1;

          then (ny + 1) = ( len g) or (( len g) + 1) = ny or ( len g) = ny by A9, A8, A51, A53, A54;

          then ny = (( len g) - 1) or ( len g) = ny by A54, NAT_1: 13;

          then x = (g . (( len g) -' 1)) or x = (g . ( len g)) by A6, A53, XREAL_1: 233;

          hence thesis by TARSKI:def 2;

        end;

        let x be object;

        

         A55: (g . ( len g)) in ( U_FT (g /. ( len g))) by A2, A8;

        (g . ((( len g) -' 1) + 1)) in ( U_FT (g /. (( len g) -' 1))) by A5, A49, A45, A48;

        then

         A56: (g . (( len g) -' 1)) in ( U_FT (g /. ( len g))) by A2, A8, A46, A48;

        assume x in {(g . (( len g) -' 1)), (g . ( len g))};

        then

         A57: x = (g . (( len g) -' 1)) or x = (g . ( len g)) by TARSKI:def 2;

        then x in ( rng g) by A7, A47, FUNCT_1:def 3;

        hence thesis by A57, A55, A56, XBOOLE_0:def 4;

      end;

    end;

    theorem :: FINTOPO6:58

    for g be FinSequence of FT, A be non empty Subset of FT, x1,x2 be Element of FT, B0 be Subset of (FT | A) st g is_minimum_path_in (A,x1,x2) & FT is filled symmetric & B0 = {x1} holds for i be Element of NAT st i < ( len g) holds (g . (i + 1)) in ( Finf (B0,i)) & (i >= 1 implies not (g . (i + 1)) in ( Finf (B0,(i -' 1))))

    proof

      let g be FinSequence of FT, A be non empty Subset of FT, x1,x2 be Element of FT, B0 be Subset of (FT | A);

      assume that

       A1: g is_minimum_path_in (A,x1,x2) and

       A2: FT is filled symmetric and

       A3: B0 = {x1};

      

       A4: ( rng g) c= A by A1;

      defpred P[ Nat] means ($1 + 1) <= ( len g) implies (g . ($1 + 1)) in ( Finf (B0,$1)) & ($1 >= 1 implies not (g . ($1 + 1)) in ( Finf (B0,($1 -' 1))));

      defpred Q[ Nat] means for y be Element of FT st y in ( Finf (B0,$1)) holds ex h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = y & ( len h) <= ($1 + 1);

      

       A5: ( [#] (FT | A)) = A by Def3;

      

       A6: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        assume

         A7: Q[k];

        for y be Element of FT st y in ( Finf (B0,(k + 1))) holds ex h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = y & ( len h) <= ((k + 1) + 1)

        proof

          let y be Element of FT;

          

           A8: ( Finf (B0,(k + 1))) = (( Finf (B0,k)) ^f ) by FINTOPO3: 31;

          assume y in ( Finf (B0,(k + 1)));

          then

          consider x be Element of (FT | A) such that

           A9: x = y and

           A10: ex y2 be Element of (FT | A) st y2 in ( Finf (B0,k)) & x in ( U_FT y2) by A8;

          

           A11: ( [#] (FT | A)) = A by Def3;

          then

           A12: {y} c= A by A9, ZFMISC_1: 31;

          consider y2 be Element of (FT | A) such that

           A13: y2 in ( Finf (B0,k)) and

           A14: x in ( U_FT y2) by A10;

          y2 in the carrier of (FT | A);

          then

          reconsider y3 = y2 as Element of FT by A11;

          consider h2 be FinSequence of FT such that

           A15: h2 is continuous and

           A16: ( rng h2) c= A and

           A17: (h2 . 1) = x1 and

           A18: (h2 . ( len h2)) = y3 and

           A19: ( len h2) <= (k + 1) by A7, A13;

          ( U_FT y2) = (( U_FT y3) /\ A) by A11, Def2;

          then

           A20: y in ( U_FT y3) by A9, A14, XBOOLE_0:def 4;

          reconsider h3 = (h2 ^ <*y*>) as FinSequence of FT;

          ( rng (h2 ^ <*y*>)) = (( rng h2) \/ ( rng <*y*>)) & ( rng <*y*>) = {y} by FINSEQ_1: 31, FINSEQ_1: 39;

          then

           A21: ( rng h3) c= A by A16, A12, XBOOLE_1: 8;

          1 <= ( len h2) by A15;

          then 1 in ( dom h2) by FINSEQ_3: 25;

          then

           A22: (h3 . 1) = x1 by A17, FINSEQ_1:def 7;

          ( len <*y*>) = 1 by FINSEQ_1: 40;

          then

           A23: ( len h3) = (( len h2) + 1) by FINSEQ_1: 22;

          then

           A24: (h3 . ( len h3)) = y by FINSEQ_1: 42;

          ( len h3) <= ((k + 1) + 1) by A19, A23, XREAL_1: 6;

          hence thesis by A15, A18, A20, A21, A22, A24, Th43;

        end;

        hence thesis;

      end;

      

       A25: (g . 1) = x1 by A1;

      then

       A26: (g . 1) in {x1} by TARSKI:def 1;

      

       A27: (g . ( len g)) = x2 by A1;

      

       A28: g is continuous by A1;

      then 1 <= ( len g);

      then 1 in ( dom g) by FINSEQ_3: 25;

      then x1 in ( rng g) by A25, FUNCT_1:def 3;

      then

       A29: {x1} c= A by A4, ZFMISC_1: 31;

      for y be Element of FT st y in ( Finf (B0, 0 )) holds ex h be FinSequence of FT st h is continuous & ( rng h) c= A & (h . 1) = x1 & (h . ( len h)) = y & ( len h) <= ( 0 + 1)

      proof

        let y be Element of FT;

        

         A30: ( len <*x1*>) = 1 by FINSEQ_1: 40;

        assume y in ( Finf (B0, 0 ));

        then y in {x1} by A3, FINTOPO3: 32;

        then

         A31: y = x1 by TARSKI:def 1;

        ( rng <*x1*>) = {x1} & ( <*x1*> . 1) = x1 by FINSEQ_1: 39, FINSEQ_1: 40;

        hence thesis by A29, A31, A30;

      end;

      then

       A32: Q[ 0 ];

      

       A33: for k be Nat holds Q[k] from NAT_1:sch 2( A32, A6);

      

       A34: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A35: P[k];

        per cases ;

          suppose ((k + 1) + 1) > ( len g);

          hence thesis;

        end;

          suppose

           A36: ((k + 1) + 1) <= ( len g);

          

           A37: 1 <= (k + 1) by NAT_1: 12;

          then 1 < ((k + 1) + 1) by NAT_1: 13;

          then ((k + 1) + 1) in ( dom g) by A36, FINSEQ_3: 25;

          then

           A38: (g . ((k + 1) + 1)) in ( rng g) by FUNCT_1:def 3;

          reconsider y0 = (g . (k + 1)) as Element of (FT | A) by A35, A36, NAT_1: 13;

          

           A39: (k + 1) < ( len g) by A36, NAT_1: 13;

          then (k + 1) in ( dom g) by A37, FINSEQ_3: 25;

          then

           A40: (g . (k + 1)) = (g /. (k + 1)) by PARTFUN1:def 6;

          1 < ((k + 1) + 1) by A37, NAT_1: 13;

          then

           A41: ((k + 1) + 1) in ( dom g) by A36, FINSEQ_3: 25;

           A42:

          now

            assume

             A43: (g . ((k + 1) + 1)) in ( Finf (B0,k));

            now

              per cases ;

                suppose

                 A44: k = 0 ;

                then (k - 1) < 0 ;

                then (k -' 1) = 0 by XREAL_0:def 2;

                then ( Finf (B0,k)) c= (( Finf (B0,(k -' 1))) ^f ) by A2, A44, FINTOPO3: 1;

                hence (g . ((k + 1) + 1)) in (( Finf (B0,(k -' 1))) ^f ) by A43;

              end;

                suppose k > 0 ;

                then k >= ( 0 + 1) by NAT_1: 13;

                then k = ((k -' 1) + 1) by XREAL_1: 235;

                hence (g . ((k + 1) + 1)) in (( Finf (B0,(k -' 1))) ^f ) by A43, FINTOPO3: 31;

              end;

            end;

            then

            consider x be Element of (FT | A) such that

             A45: (g . ((k + 1) + 1)) = x and ex y be Element of (FT | A) st y in ( Finf (B0,(k -' 1))) & x in ( U_FT y);

            x in A by A5;

            then

            reconsider x3 = x as Element of FT;

            consider h be FinSequence of FT such that

             A46: h is continuous and

             A47: ( rng h) c= A and

             A48: (h . 1) = x1 and

             A49: (h . ( len h)) = x3 and

             A50: ( len h) <= (k + 1) by A33, A43, A45;

            reconsider s = (h ^ (g /^ ((k + 1) + 1))) as FinSequence of FT;

            

             A51: ( len s) = (( len h) + ( len (g /^ ((k + 1) + 1)))) by FINSEQ_1: 22;

            g = ((g | ((k + 1) + 1)) ^ (g /^ ((k + 1) + 1))) by RFINSEQ: 8;

            then

             A52: ( len g) = (( len (g | ((k + 1) + 1))) + ( len (g /^ ((k + 1) + 1)))) by FINSEQ_1: 22;

            

             A53: 1 <= ( len h) by A46;

            then ( len h) in ( dom h) by FINSEQ_3: 25;

            then

             A54: (h . ( len h)) = (h /. ( len h)) by PARTFUN1:def 6;

            ( len (g | ((k + 1) + 1))) = ((k + 1) + 1) by A36, FINSEQ_1: 59;

            then

             A55: ( len (g | ((k + 1) + 1))) > ( len h) by A50, NAT_1: 13;

            then

             A56: ( len s) < ( len g) by A51, A52, XREAL_1: 8;

            per cases ;

              suppose

               A57: ((k + 1) + 1) < ( len g);

              then ( len g) >= (1 + ((k + 1) + 1)) by NAT_1: 13;

              then 1 <= (( len g) - ((k + 1) + 1)) by XREAL_1: 19;

              then 1 <= ( len (g /^ ((k + 1) + 1))) by A57, RFINSEQ:def 1;

              then

               A58: 1 in ( dom (g /^ ((k + 1) + 1))) by FINSEQ_3: 25;

              

               A59: (g . ((k + 1) + 1)) = (g /. ((k + 1) + 1)) by A41, PARTFUN1:def 6;

              

               A60: (g /^ ((k + 1) + 1)) is continuous by A28, A57, Th47;

              then 1 <= ( len (g /^ ((k + 1) + 1)));

              then ( len (g /^ ((k + 1) + 1))) in ( dom (g /^ ((k + 1) + 1))) by FINSEQ_3: 25;

              

              then

               A61: (s . ( len s)) = ((g /^ ((k + 1) + 1)) . ( len (g /^ ((k + 1) + 1)))) by A51, FINSEQ_1:def 7

              .= x2 by A27, A57, JORDAN4: 6;

              1 <= ((k + 1) + 1) by NAT_1: 12;

              then (g . (((k + 1) + 1) + 1)) in ( U_FT (g /. ((k + 1) + 1))) by A28, A57, A59;

              then ((g /^ ((k + 1) + 1)) . 1) in ( U_FT (h /. ( len h))) by A45, A49, A54, A57, A59, A58, RFINSEQ:def 1;

              then

               A62: s is continuous by A46, A60, Th44;

              1 in ( dom h) by A53, FINSEQ_3: 25;

              then

               A63: (s . 1) = x1 by A48, FINSEQ_1:def 7;

              ( rng (g /^ ((k + 1) + 1))) c= ( rng g) by FINSEQ_5: 33;

              then

               A64: ( rng (g /^ ((k + 1) + 1))) c= A by A4;

              ( rng s) = (( rng h) \/ ( rng (g /^ ((k + 1) + 1)))) by FINSEQ_1: 31;

              then ( rng s) c= A by A47, A64, XBOOLE_1: 8;

              hence contradiction by A1, A56, A62, A63, A61;

            end;

              suppose

               A65: ((k + 1) + 1) >= ( len g);

              then (g /^ ((k + 1) + 1)) = ( <*> the carrier of FT) by FINSEQ_5: 32;

              then

               A66: s = h by FINSEQ_1: 34;

              ((k + 1) + 1) = ( len g) by A36, A65, XXREAL_0: 1;

              hence contradiction by A1, A45, A46, A47, A48, A49, A55, A51, A52, A66;

            end;

          end;

          ( [#] (FT | A)) = A by Def3;

          then

           A67: ( U_FT y0) = (( U_FT (g /. (k + 1))) /\ A) by A40, Def2;

          (g . ((k + 1) + 1)) in ( U_FT (g /. (k + 1))) by A28, A39, A37, A40;

          then (g . ((k + 1) + 1)) in ( U_FT y0) by A4, A67, A38, XBOOLE_0:def 4;

          then

           A68: (g . ((k + 1) + 1)) in (( Finf (B0,k)) ^f ) by A35, A36, NAT_1: 13;

          ((k + 1) -' 1) = ((k + 1) - 1) by NAT_D: 37

          .= k;

          hence thesis by A68, A42, FINTOPO3: 31;

        end;

      end;

      let i be Element of NAT ;

      assume i < ( len g);

      then

       A69: (i + 1) <= ( len g) by NAT_1: 13;

      ( Finf ( {x1}, 0 )) = {x1} by FINTOPO3: 32

      .= ( Finf (B0, 0 )) by A3, FINTOPO3: 32;

      then

       A70: P[ 0 ] by A26, FINTOPO3: 32;

      for j be Nat holds P[j] from NAT_1:sch 2( A70, A34);

      hence thesis by A69;

    end;