fintopo4.miz



    begin

    definition

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

      :: FINTOPO4:def1

      pred A,B are_separated means (A ^b ) misses B & A misses (B ^b );

      symmetry ;

    end

    theorem :: FINTOPO4:1

    

     Th1: for FT be filled non empty RelStr, A be Subset of FT, n,m be Element of NAT st n <= m holds ( Finf (A,n)) c= ( Finf (A,m))

    proof

      let FT be filled non empty RelStr, A be Subset of FT, n,m be Element of NAT ;

      defpred P[ Nat] means ( Finf (A,n)) c= ( Finf (A,(n + $1)));

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        

         A2: ( Finf (A,(n + k))) c= ( Finf (A,((n + k) + 1))) by FINTOPO3: 37;

        assume P[k];

        hence thesis by A2, XBOOLE_1: 1;

      end;

      assume n <= m;

      then (m - n) >= 0 by XREAL_1: 48;

      

      then

       A3: (n + (m -' n)) = (n + (m - n)) by XREAL_0:def 2

      .= m;

      

       A4: P[ 0 ];

      for m2 be Nat holds P[m2] from NAT_1:sch 2( A4, A1);

      hence thesis by A3;

    end;

    theorem :: FINTOPO4:2

    for FT be filled non empty RelStr, A be Subset of FT, n,m be Element of NAT st n <= m holds ( Fcl (A,n)) c= ( Fcl (A,m))

    proof

      let FT be filled non empty RelStr, A be Subset of FT, n,m be Element of NAT ;

      defpred P[ Nat] means ( Fcl (A,n)) c= ( Fcl (A,(n + $1)));

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        

         A2: ( Fcl (A,(n + k))) c= ( Fcl (A,((n + k) + 1))) by FINTOPO3: 25;

        assume P[k];

        hence thesis by A2, XBOOLE_1: 1;

      end;

      assume n <= m;

      then (m - n) >= 0 by XREAL_1: 48;

      

      then

       A3: (n + (m -' n)) = (n + (m - n)) by XREAL_0:def 2

      .= m;

      

       A4: P[ 0 ];

      for m2 be Nat holds P[m2] from NAT_1:sch 2( A4, A1);

      hence thesis by A3;

    end;

    theorem :: FINTOPO4:3

    for FT be filled non empty RelStr, A be Subset of FT, n,m be Element of NAT st n <= m holds ( Fdfl (A,m)) c= ( Fdfl (A,n))

    proof

      let FT be filled non empty RelStr, A be Subset of FT, n,m be Element of NAT ;

      defpred P[ Nat] means ( Fdfl (A,(n + $1))) c= ( Fdfl (A,n));

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        

         A2: ( Fdfl (A,((n + k) + 1))) c= ( Fdfl (A,(n + k))) by FINTOPO3: 44;

        assume P[k];

        hence thesis by A2, XBOOLE_1: 1;

      end;

      assume n <= m;

      then (m - n) >= 0 by XREAL_1: 48;

      

      then

       A3: (n + (m -' n)) = (n + (m - n)) by XREAL_0:def 2

      .= m;

      

       A4: P[ 0 ];

      for m2 be Nat holds P[m2] from NAT_1:sch 2( A4, A1);

      hence thesis by A3;

    end;

    theorem :: FINTOPO4:4

    for FT be filled non empty RelStr, A be Subset of FT, n,m be Element of NAT st n <= m holds ( Fint (A,m)) c= ( Fint (A,n))

    proof

      let FT be filled non empty RelStr, A be Subset of FT, n,m be Element of NAT ;

      defpred P[ Nat] means ( Fint (A,(n + $1))) c= ( Fint (A,n));

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        

         A2: ( Fint (A,((n + k) + 1))) c= ( Fint (A,(n + k))) by FINTOPO3: 26;

        assume P[k];

        hence thesis by A2, XBOOLE_1: 1;

      end;

      assume n <= m;

      then (m - n) >= 0 by XREAL_1: 48;

      

      then

       A3: (n + (m -' n)) = (n + (m - n)) by XREAL_0:def 2

      .= m;

      

       A4: P[ 0 ];

      for m2 be Nat holds P[m2] from NAT_1:sch 2( A4, A1);

      hence thesis by A3;

    end;

    theorem :: FINTOPO4:5

    for FT be non empty RelStr, A,B be Subset of FT st (A,B) are_separated holds (B,A) are_separated ;

    theorem :: FINTOPO4:6

    

     Th6: for FT be filled non empty RelStr, A,B be Subset of FT st (A,B) are_separated holds A misses B by FIN_TOPO: 13, XBOOLE_1: 63;

    theorem :: FINTOPO4:7

    for FT be non empty RelStr, A,B be Subset of FT st FT is symmetric holds (A,B) are_separated iff (A ^f ) misses B & A misses (B ^f ) by FIN_TOPO: 12;

    theorem :: FINTOPO4:8

    

     Th8: for FT be filled non empty RelStr, A,B be Subset of FT st FT is symmetric & (A ^b ) misses B holds A misses (B ^b )

    proof

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

      assume that

       A1: FT is symmetric and

       A2: (A ^b ) misses B;

      now

        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 x2 be Element of FT such that

         A5: x2 = x and

         A6: ( U_FT x2) meets B by A4;

        set y = the Element of (( U_FT x2) /\ B);

        

         A7: (( U_FT x2) /\ B) <> {} by A6, XBOOLE_0:def 7;

        then

         A8: y in ( U_FT x2) by XBOOLE_0:def 4;

        then

        reconsider y2 = y as Element of FT;

        x2 in ( U_FT y2) by A1, A8;

        then x2 in (( U_FT y2) /\ A) by A3, A5, XBOOLE_0:def 4;

        then ( U_FT y2) meets A by XBOOLE_0:def 7;

        then

         A9: y2 in (A ^b );

        y in B by A7, XBOOLE_0:def 4;

        hence contradiction by A2, A9, XBOOLE_0: 3;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO4:9

    for FT be filled non empty RelStr, A,B be Subset of FT st FT is symmetric & A misses (B ^b ) holds (A ^b ) misses B by Th8;

    theorem :: FINTOPO4:10

    for FT be filled non empty RelStr, A,B be Subset of FT st FT is symmetric holds (A,B) are_separated iff (A ^b ) misses B by Th8;

    theorem :: FINTOPO4:11

    for FT be filled non empty RelStr, A,B be Subset of FT st FT is symmetric holds (A,B) are_separated iff A misses (B ^b ) by Th8;

    theorem :: FINTOPO4:12

    

     Th12: for FT be filled non empty RelStr, IT be Subset of FT st FT is symmetric holds IT is connected iff (for A,B be Subset of FT st IT = (A \/ B) & (A,B) are_separated holds A = IT or B = IT)

    proof

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

      assume

       A1: FT is symmetric;

       A2:

      now

        assume

         A3: for A,B be Subset of FT st IT = (A \/ B) & (A,B) are_separated holds A = IT or B = IT;

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

        proof

          let A,B be Subset of FT;

          assume that

           A4: IT = (A \/ B) and

           A5: A <> {} & B <> {} and A misses B;

          now

            assume

             A6: (A ^b ) misses B;

            now

              assume A meets (B ^b );

              then

              consider x be object such that

               A7: x in A and

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

              consider x2 be Element of FT such that

               A9: x2 = x and

               A10: ( U_FT x2) meets B by A8;

              set y = the Element of (( U_FT x2) /\ B);

              

               A11: (( U_FT x2) /\ B) <> {} by A10, XBOOLE_0:def 7;

              then

               A12: y in ( U_FT x2) by XBOOLE_0:def 4;

              then

              reconsider y2 = y as Element of FT;

              x2 in ( U_FT y2) by A1, A12;

              then x2 in (( U_FT y2) /\ A) by A7, A9, XBOOLE_0:def 4;

              then ( U_FT y2) meets A by XBOOLE_0:def 7;

              then

               A13: y2 in (A ^b );

              y in B by A11, XBOOLE_0:def 4;

              hence contradiction by A6, A13, XBOOLE_0: 3;

            end;

            then (A,B) are_separated by A6;

            then

             A14: A = IT or B = IT by A3, A4;

            

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

            ((A ^b ) /\ B) = {} by A6, XBOOLE_0:def 7;

            then (A /\ B) = {} by A15, XBOOLE_1: 3, XBOOLE_1: 26;

            hence contradiction by A4, A5, A14, XBOOLE_1: 21;

          end;

          hence thesis;

        end;

        hence IT is connected;

      end;

      now

        assume

         A16: IT is connected;

        thus for A,B be Subset of FT st IT = (A \/ B) & (A,B) are_separated holds A = IT or B = IT

        proof

          let A,B be Subset of FT;

          assume that

           A17: IT = (A \/ B) and

           A18: (A,B) are_separated ;

          

           A19: A misses B by A18, Th6;

          now

            assume A <> {} ;

            then B = {} by A18, A16, A17, A19;

            hence thesis by A17;

          end;

          hence thesis by A17;

        end;

      end;

      hence thesis by A2;

    end;

    theorem :: FINTOPO4:13

    for FT be filled non empty RelStr, B be Subset of FT st FT is symmetric holds B is connected iff not (ex C be Subset of FT st C <> {} & (B \ C) <> {} & C c= B & (C ^b ) misses (B \ C))

    proof

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

      assume

       A1: FT is symmetric;

      thus B is connected implies not (ex C be Subset of FT st C <> {} & (B \ C) <> {} & C c= B & (C ^b ) misses (B \ C))

      proof

        assume

         A2: B is connected;

        for C be Subset of FT st C c= B & (C ^b ) misses (B \ C) holds C = {} or (B \ C) = {}

        proof

          let C be Subset of FT;

          assume that

           A3: C c= B and

           A4: (C ^b ) misses (B \ C);

          C misses ((B \ C) ^b ) by A1, A4, Th8;

          then

           A5: (C,(B \ C)) are_separated by A4;

          (C \/ (B \ C)) = (C \/ B) by XBOOLE_1: 39

          .= B by A3, XBOOLE_1: 12;

          then C = B or (B \ C) = B by A1, A2, A5, Th12;

          hence thesis by A3, XBOOLE_1: 37, XBOOLE_1: 38;

        end;

        hence thesis;

      end;

      thus not (ex C be Subset of FT st C <> {} & (B \ C) <> {} & C c= B & (C ^b ) misses (B \ C)) implies B is connected

      proof

        assume

         A6: not (ex C be Subset of FT st C <> {} & (B \ C) <> {} & C c= B & (C ^b ) misses (B \ C));

        for A,B2 be Subset of FT st B = (A \/ B2) & (A,B2) are_separated holds A = B or B2 = B

        proof

          let A,B2 be Subset of FT;

          assume that

           A7: B = (A \/ B2) and

           A8: (A,B2) are_separated ;

          

           A9: ((A \/ B2) \ A) = (B2 \ A) by XBOOLE_1: 40;

          (A ^b ) misses B2 by A8;

          then (A ^b ) misses (B \ A) by A7, A9, XBOOLE_1: 36, XBOOLE_1: 63;

          then A = {} or (B \ A) = {} by A6, A7, XBOOLE_1: 7;

          then

           A10: B = B2 or B c= A by A7, XBOOLE_1: 37;

          A c= B by A7, XBOOLE_1: 7;

          hence thesis by A10, XBOOLE_0:def 10;

        end;

        hence thesis by A1, Th12;

      end;

    end;

    definition

      let FT1,FT2 be non empty RelStr, f be Function of FT1, FT2, n be Nat;

      :: FINTOPO4:def2

      pred f is_continuous n means for x be Element of FT1, y be Element of FT2 st x in the carrier of FT1 & y = (f . x) holds (f .: ( U_FT (x, 0 ))) c= ( U_FT (y,n));

    end

    theorem :: FINTOPO4:14

    for FT1 be non empty RelStr, FT2 be filled non empty RelStr, n be Element of NAT , f be Function of FT1, FT2 st f is_continuous 0 holds f is_continuous n

    proof

      let FT1 be non empty RelStr, FT2 be filled non empty RelStr, n be Element of NAT , f be Function of FT1, FT2;

      assume

       A1: f is_continuous 0 ;

      for x be Element of FT1, y be Element of FT2 st x in the carrier of FT1 & y = (f . x) holds (f .: ( U_FT (x, 0 ))) c= ( U_FT (y,n))

      proof

        let x be Element of FT1, y be Element of FT2;

        assume that x in the carrier of FT1 and

         A2: y = (f . x);

        ( U_FT y) = ( U_FT (y, 0 )) & ( U_FT (y,n)) = ( Finf (( U_FT y),n)) by FINTOPO3: 47, FINTOPO3:def 10;

        then

         A3: ( U_FT (y, 0 )) c= ( U_FT (y,n)) by FINTOPO3: 36;

        (f .: ( U_FT (x, 0 ))) c= ( U_FT (y, 0 )) by A1, A2;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO4:15

    for FT1 be non empty RelStr, FT2 be filled non empty RelStr, n0,n be Element of NAT , f be Function of FT1, FT2 st f is_continuous n0 & n0 <= n holds f is_continuous n

    proof

      let FT1 be non empty RelStr, FT2 be filled non empty RelStr, n0,n be Element of NAT , f be Function of FT1, FT2;

      assume that

       A1: f is_continuous n0 and

       A2: n0 <= n;

      for x be Element of FT1, y be Element of FT2 st x in the carrier of FT1 & y = (f . x) holds (f .: ( U_FT (x, 0 ))) c= ( U_FT (y,n))

      proof

        let x be Element of FT1, y be Element of FT2;

        assume that x in the carrier of FT1 and

         A3: y = (f . x);

        ( U_FT (y,n0)) = ( Finf (( U_FT y),n0)) & ( U_FT (y,n)) = ( Finf (( U_FT y),n)) by FINTOPO3:def 10;

        then

         A4: ( U_FT (y,n0)) c= ( U_FT (y,n)) by A2, Th1;

        (f .: ( U_FT (x, 0 ))) c= ( U_FT (y,n0)) by A1, A3;

        hence thesis by A4;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO4:16

    

     Th16: for FT1,FT2 be non empty RelStr, A be Subset of FT1, B be Subset of FT2, f be Function of FT1, FT2 st f is_continuous 0 & B = (f .: A) holds (f .: (A ^b )) c= (B ^b )

    proof

      let FT1,FT2 be non empty RelStr, A be Subset of FT1, B be Subset of FT2, f be Function of FT1, FT2;

      assume that

       A1: f is_continuous 0 and

       A2: B = (f .: A);

      thus (f .: (A ^b )) c= (B ^b )

      proof

        let y be object;

        assume y in (f .: (A ^b ));

        then

        consider x be object such that

         A3: x in ( dom f) and

         A4: x in (A ^b ) and

         A5: y = (f . x) by FUNCT_1:def 6;

        reconsider x0 = x as Element of FT1 by A3;

        reconsider y0 = y as Element of FT2 by A3, A5, FUNCT_2: 5;

        (f .: ( U_FT (x0, 0 ))) c= ( U_FT (y0, 0 )) by A1, A5;

        then (f .: ( U_FT x0)) c= ( U_FT (y0, 0 )) by FINTOPO3: 47;

        then (f .: ( U_FT x0)) c= ( U_FT y0) by FINTOPO3: 47;

        then

         A6: (f .: (( U_FT x0) /\ A)) c= ((f .: ( U_FT x0)) /\ (f .: A)) & ((f .: ( U_FT x0)) /\ (f .: A)) c= (( U_FT y0) /\ (f .: A)) by RELAT_1: 121, XBOOLE_1: 26;

        ex z be Element of FT1 st z = x & ( U_FT z) meets A by A4;

        then

         A7: (( U_FT x0) /\ A) <> {} by XBOOLE_0:def 7;

        ( dom f) = the carrier of FT1 by FUNCT_2:def 1;

        then (f .: (( U_FT x0) /\ A)) <> {} by A7, RELAT_1: 119;

        then (( U_FT y0) /\ (f .: A)) <> {} by A6;

        then ( U_FT y0) meets B by A2, XBOOLE_0:def 7;

        hence thesis;

      end;

    end;

    theorem :: FINTOPO4:17

    for FT1,FT2 be non empty RelStr, A be Subset of FT1, B be Subset of FT2, f be Function of FT1, FT2 st A is connected & f is_continuous 0 & B = (f .: A) holds B is connected

    proof

      let FT1,FT2 be non empty RelStr, A be Subset of FT1, B be Subset of FT2, f be Function of FT1, FT2;

      assume that

       A1: A is connected and

       A2: f is_continuous 0 and

       A3: B = (f .: A);

      for B2,C2 be Subset of FT2 st B = (B2 \/ C2) & B2 <> {} & C2 <> {} & B2 misses C2 holds (B2 ^b ) meets C2

      proof

        let B2,C2 be Subset of FT2;

        assume that

         A4: B = (B2 \/ C2) and

         A5: B2 <> {} and

         A6: C2 <> {} and

         A7: B2 misses C2;

        reconsider C1 = (f " C2) as Subset of FT1;

        reconsider C10 = (C1 /\ A) as Subset of FT1;

        reconsider B1 = (f " B2) as Subset of FT1;

        reconsider B10 = (B1 /\ A) as Subset of FT1;

        

         A8: C10 c= C1 by XBOOLE_1: 17;

        set x6 = the Element of C2;

        x6 in B by A4, A6, XBOOLE_0:def 3;

        then

        consider z6 be object such that

         A9: z6 in ( dom f) and

         A10: z6 in A and

         A11: x6 = (f . z6) by A3, FUNCT_1:def 6;

        z6 in (f " C2) by A6, A9, A11, FUNCT_1:def 7;

        then

         A12: C10 <> {} by A10, XBOOLE_0:def 4;

        set x5 = the Element of B2;

        x5 in B by A4, A5, XBOOLE_0:def 3;

        then

        consider z5 be object such that

         A13: z5 in ( dom f) and

         A14: z5 in A and

         A15: x5 = (f . z5) by A3, FUNCT_1:def 6;

        A c= the carrier of FT1;

        then

         A16: A c= ( dom f) by FUNCT_2:def 1;

        (B2 /\ C2) = {} by A7, XBOOLE_0:def 7;

        then (f " (B2 /\ C2)) = {} ;

        then B10 c= B1 & ((f " B2) /\ (f " C2)) = {} by FUNCT_1: 68, XBOOLE_1: 17;

        then (B10 /\ C10) = {} by A8, XBOOLE_1: 3, XBOOLE_1: 27;

        then

         A17: B10 misses C10 by XBOOLE_0:def 7;

        ((f " B2) \/ (f " C2)) = (f " (f .: A)) by A3, A4, RELAT_1: 140;

        then A c= (B1 \/ C1) by A16, FUNCT_1: 76;

        then A c= (A /\ (B1 \/ C1)) by XBOOLE_1: 19;

        then

         A18: A c= (B10 \/ C10) by XBOOLE_1: 23;

        B10 c= A & C10 c= A by XBOOLE_1: 17;

        then (B10 \/ C10) c= A by XBOOLE_1: 8;

        then

         A19: A = (B10 \/ C10) by A18, XBOOLE_0:def 10;

        z5 in (f " B2) by A5, A13, A15, FUNCT_1:def 7;

        then B10 <> {} by A14, XBOOLE_0:def 4;

        then (B10 ^b ) meets C10 by A1, A19, A12, A17;

        then

         A20: ((B10 ^b ) /\ C10) <> {} by XBOOLE_0:def 7;

        reconsider B20 = (f .: B1) as Subset of FT2;

        

         A21: ( dom f) = the carrier of FT1 by FUNCT_2:def 1;

        (f .: B1) c= B2

        proof

          let y be object;

          assume y in (f .: B1);

          then ex x2 be object st x2 in ( dom f) & x2 in B1 & y = (f . x2) by FUNCT_1:def 6;

          hence thesis by FUNCT_1:def 7;

        end;

        then

         A22: (B20 ^b ) c= (B2 ^b ) by FIN_TOPO: 14;

        (f .: (B1 ^b )) c= (B20 ^b ) by A2, Th16;

        then (f .: (B1 ^b )) c= (B2 ^b ) by A22;

        then

         A23: ((f .: (B1 ^b )) /\ (f .: C1)) c= ((f .: (B1 ^b )) /\ C2) & ((f .: (B1 ^b )) /\ C2) c= ((B2 ^b ) /\ C2) by FUNCT_1: 75, XBOOLE_1: 26;

        (B10 ^b ) c= (B1 ^b ) by FIN_TOPO: 14, XBOOLE_1: 17;

        then ((B1 ^b ) /\ C1) <> {} by A8, A20, XBOOLE_1: 3, XBOOLE_1: 27;

        then (f .: ((B1 ^b ) /\ C1)) <> {} by A21, RELAT_1: 119;

        then ((f .: (B1 ^b )) /\ (f .: C1)) <> {} by RELAT_1: 121, XBOOLE_1: 3;

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

        hence thesis by XBOOLE_0:def 7;

      end;

      hence thesis;

    end;

    definition

      let n be Nat;

      :: FINTOPO4:def3

      func Nbdl1 n -> Relation of ( Seg n) means

      : Def3: for i be Element of NAT st i in ( Seg n) holds ( Im (it ,i)) = {i, ( max ((i -' 1),1)), ( min ((i + 1),n))};

      existence

      proof

        deffunc F( Nat) = {$1, ( max (($1 -' 1),1)), ( min (($1 + 1),n))};

        

         A1: for x be Element of NAT st x in ( Seg n) holds F(x) c= ( Seg n)

        proof

          let i be Element of NAT ;

          set y0 = {i, ( max ((i -' 1),1)), ( min ((i + 1),n))};

          assume

           A2: i in ( Seg n);

          then ( Seg n) <> {} ;

          then n > 0 ;

          then

           A3: ( 0 + 1) <= n by NAT_1: 13;

          thus y0 c= ( Seg n)

          proof

            let z1 be object;

            assume

             A4: z1 in y0;

            then z1 = i or z1 = ( max ((i -' 1),1)) or z1 = ( min ((i + 1),n)) by ENUMSET1:def 1;

            then

            reconsider z2 = z1 as Element of NAT by ORDINAL1:def 12;

             A5:

            now

              (i -' 1) <= i & i <= n by A2, FINSEQ_1: 1, NAT_D: 35;

              then (i -' 1) <= n by XXREAL_0: 2;

              then

               A6: 1 <= ( max ((i -' 1),1)) & ( max ((i -' 1),1)) <= n by A3, XXREAL_0: 28, XXREAL_0: 30;

              assume z1 = ( max ((i -' 1),1));

              hence thesis by A6;

            end;

            now

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

              then

               A7: 1 <= ( min ((i + 1),n)) by A3, XXREAL_0: 20;

              

               A8: ( min ((i + 1),n)) <= n by XXREAL_0: 17;

              assume z1 = ( min ((i + 1),n));

              hence z2 in ( Seg n) by A7, A8;

            end;

            hence thesis by A2, A4, A5, ENUMSET1:def 1;

          end;

        end;

        consider f be Relation of ( Seg n) such that

         A9: for x3 be Element of NAT st x3 in ( Seg n) holds ( Im (f,x3)) = F(x3) from RELSET_1:sch 3( A1);

        take f;

        thus thesis by A9;

      end;

      uniqueness

      proof

        thus for f1,f2 be Relation of ( Seg n) st (for i be Element of NAT st i in ( Seg n) holds ( Im (f1,i)) = {i, ( max ((i -' 1),1)), ( min ((i + 1),n))}) & (for i be Element of NAT st i in ( Seg n) holds ( Im (f2,i)) = {i, ( max ((i -' 1),1)), ( min ((i + 1),n))}) holds f1 = f2

        proof

          let f1,f2 be Relation of ( Seg n);

          assume that

           A10: for i be Element of NAT st i in ( Seg n) holds ( Im (f1,i)) = {i, ( max ((i -' 1),1)), ( min ((i + 1),n))} and

           A11: for i be Element of NAT st i in ( Seg n) holds ( Im (f2,i)) = {i, ( max ((i -' 1),1)), ( min ((i + 1),n))};

          for x be set st x in ( Seg n) holds ( Im (f1,x)) = ( Im (f2,x))

          proof

            let x be set;

            assume

             A12: x in ( Seg n);

            then

            reconsider i2 = x as Element of NAT ;

            ( Im (f1,i2)) = {i2, ( max ((i2 -' 1),1)), ( min ((i2 + 1),n))} by A10, A12;

            hence thesis by A11, A12;

          end;

          hence thesis by RELSET_1: 31;

        end;

      end;

    end

    definition

      let n be Nat;

      assume

       A1: n > 0 ;

      :: FINTOPO4:def4

      func FTSL1 n -> non empty RelStr equals

      : Def4: RelStr (# ( Seg n), ( Nbdl1 n) #);

      correctness by A1;

    end

    theorem :: FINTOPO4:18

    for n be Nat st n > 0 holds ( FTSL1 n) is filled

    proof

      let n be Nat;

      assume n > 0 ;

      then

       A1: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by Def4;

      let x be Element of ( FTSL1 n);

      x in ( Seg n) by A1;

      then

      reconsider i = x as Element of NAT ;

      ( U_FT x) = {i, ( max ((i -' 1),1)), ( min ((i + 1),n))} by A1, Def3;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: FINTOPO4:19

    for n be Nat st n > 0 holds ( FTSL1 n) is symmetric

    proof

      let n be Nat;

      assume n > 0 ;

      then

       A1: ( FTSL1 n) = RelStr (# ( Seg n), ( Nbdl1 n) #) by Def4;

      let x,y be Element of ( FTSL1 n);

      x in ( Seg n) by A1;

      then

      reconsider i = x as Element of NAT ;

      

       A2: 1 <= i by A1, FINSEQ_1: 1;

      

       A3: i <= n by A1, FINSEQ_1: 1;

      y in ( Seg n) by A1;

      then

      reconsider j = y as Element of NAT ;

      

       A4: ( U_FT y) = {j, ( max ((j -' 1),1)), ( min ((j + 1),n))} by A1, Def3;

      

       A5: ( U_FT x) = {i, ( max ((i -' 1),1)), ( min ((i + 1),n))} by A1, Def3;

      now

         A6:

        now

          assume

           A7: y = ( max ((i -' 1),1));

          now

            per cases ;

              case

               A8: (i -' 1) >= 1;

              then

               A9: y = (i -' 1) by A7, XXREAL_0:def 10;

              now

                per cases ;

                  case (i - 1) >= 0 ;

                  then j = (i - 1) by A9, XREAL_0:def 2;

                  hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n)) by A3, XXREAL_0:def 9;

                end;

                  case (i - 1) < 0 ;

                  hence contradiction by A8, XREAL_0:def 2;

                end;

              end;

              hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n));

            end;

              case

               A10: (i -' 1) < 1;

               A11:

              now

                assume i > 1;

                then

                 A12: (i - 1) > 0 by XREAL_1: 50;

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

                then (i -' 1) >= ( 0 + 1) by A12, NAT_1: 13;

                hence contradiction by A10;

              end;

              y = 1 by A7, A10, XXREAL_0:def 10;

              hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n)) by A2, A11, XXREAL_0: 1;

            end;

          end;

          hence x in ( U_FT y) by A4, ENUMSET1:def 1;

        end;

        assume

         A13: y in ( U_FT x);

         A14:

        now

          assume y = ( min ((i + 1),n));

          now

            per cases by A5, A13, ENUMSET1:def 1;

              case y = i;

              hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n));

            end;

              case

               A15: y = ( max ((i -' 1),1));

              now

                per cases ;

                  case

                   A16: (i -' 1) >= 1;

                  then

                   A17: y = (i -' 1) by A15, XXREAL_0:def 10;

                  now

                    per cases ;

                      case (i - 1) >= 0 ;

                      then j = (i - 1) by A17, XREAL_0:def 2;

                      hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n)) by A3, XXREAL_0:def 9;

                    end;

                      case (i - 1) < 0 ;

                      hence contradiction by A16, XREAL_0:def 2;

                    end;

                  end;

                  hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n));

                end;

                  case

                   A18: (i -' 1) < 1;

                   A19:

                  now

                    assume i > 1;

                    then

                     A20: (i - 1) > 0 by XREAL_1: 50;

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

                    then (i -' 1) >= ( 0 + 1) by A20, NAT_1: 13;

                    hence contradiction by A18;

                  end;

                  y = 1 by A15, A18, XXREAL_0:def 10;

                  hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n)) by A2, A19, XXREAL_0: 1;

                end;

              end;

              hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n));

            end;

              case

               A21: y = ( min ((i + 1),n));

              now

                per cases ;

                  case (i + 1) <= n;

                  then

                   A22: y = (i + 1) by A21, XXREAL_0:def 9;

                  then

                   A23: (j - 1) = (j -' 1) by XREAL_0:def 2;

                  now

                    per cases ;

                      case (j - 1) >= 1;

                      hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n)) by A22, A23, XXREAL_0:def 10;

                    end;

                      case (j - 1) < 1;

                      hence contradiction by A1, A22, FINSEQ_1: 1;

                    end;

                  end;

                  hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n));

                end;

                  case

                   A24: (i + 1) > n;

                  then y = n by A21, XXREAL_0:def 9;

                  then (j + 1) > n by NAT_1: 13;

                  then

                   A25: ( min ((j + 1),n)) = n by XXREAL_0:def 9;

                  i >= n by A24, NAT_1: 13;

                  hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n)) by A3, A25, XXREAL_0: 1;

                end;

              end;

              hence x = j or x = ( max ((j -' 1),1)) or x = ( min ((j + 1),n));

            end;

          end;

          hence x in ( U_FT y) by A4, ENUMSET1:def 1;

        end;

        y = i or y = ( max ((i -' 1),1)) or y = ( min ((i + 1),n)) by A5, A13, ENUMSET1:def 1;

        hence x in ( U_FT y) by A13, A6, A14;

      end;

      hence thesis;

    end;

    definition

      let n be Nat;

      :: FINTOPO4:def5

      func Nbdc1 n -> Relation of ( Seg n) means

      : Def5: for i be Element of NAT st i in ( Seg n) holds (1 < i & i < n implies ( Im (it ,i)) = {i, (i -' 1), (i + 1)}) & (i = 1 & i < n implies ( Im (it ,i)) = {i, n, (i + 1)}) & (1 < i & i = n implies ( Im (it ,i)) = {i, (i -' 1), 1}) & (i = 1 & i = n implies ( Im (it ,i)) = {i});

      existence

      proof

        defpred P[ object, object] means for i be Element of NAT st i = $1 holds (1 < i & i < n implies $2 = {i, (i -' 1), (i + 1)}) & (i = 1 & i < n implies $2 = {i, n, (i + 1)}) & (1 < i & i = n implies $2 = {i, (i -' 1), 1}) & (i = 1 & i = n implies $2 = {i});

        

         A1: for x be object st x in ( Seg n) holds ex y be object st y in ( bool ( Seg n)) & P[x, y]

        proof

          let x be object;

          assume

           A2: x in ( Seg n);

          then

          reconsider i2 = x as Element of NAT ;

          

           A3: 1 <= i2 & i2 <= n by A2, FINSEQ_1: 1;

          now

            per cases by A3, XXREAL_0: 1;

              case

               A4: 1 < i2 & i2 < n;

              i2 <= (i2 + 1) by NAT_1: 12;

              then

               A5: 1 < (i2 + 1) by A4, XXREAL_0: 2;

              (i2 + 1) <= n by A4, NAT_1: 13;

              then

               A6: (i2 + 1) in ( Seg n) by A5;

              set y0 = {i2, (i2 -' 1), (i2 + 1)};

              (i2 - 1) > 0 by A4, XREAL_1: 50;

              then (i2 -' 1) > 0 by XREAL_0:def 2;

              then

               A7: (i2 -' 1) >= ( 0 + 1) by NAT_1: 13;

              (i2 -' 1) <= i2 by NAT_D: 35;

              then (i2 -' 1) < n by A4, XXREAL_0: 2;

              then

               A8: (i2 -' 1) in ( Seg n) by A7;

              

               A9: y0 c= ( Seg n) by A2, A8, A6, ENUMSET1:def 1;

               P[x, y0] by A4;

              hence thesis by A9;

            end;

              case

               A10: i2 = 1 & i2 < n;

              then (i2 + 1) <= n by NAT_1: 13;

              then

               A11: (i2 + 1) in ( Seg n) by A10;

              set y0 = {i2, n, (i2 + 1)};

              

               A12: n in ( Seg n) by A10;

              

               A13: y0 c= ( Seg n) by A2, A12, A11, ENUMSET1:def 1;

               P[x, y0] by A10;

              hence thesis by A13;

            end;

              case

               A14: 1 < i2 & i2 = n;

              then (i2 - 1) > 0 by XREAL_1: 50;

              then (i2 -' 1) > 0 by XREAL_0:def 2;

              then

               A15: (i2 -' 1) >= ( 0 + 1) by NAT_1: 13;

              set y0 = {i2, (i2 -' 1), 1};

              

               A16: 1 in ( Seg n) by A14;

              (i2 -' 1) <= n by A14, NAT_D: 35;

              then

               A17: (i2 -' 1) in ( Seg n) by A15;

              

               A18: y0 c= ( Seg n) by A2, A17, A16, ENUMSET1:def 1;

               P[x, y0] by A14;

              hence thesis by A18;

            end;

              case

               A19: i2 = 1 & i2 = n;

              set y0 = {i2};

              

               A20: y0 c= ( Seg n) by A2, TARSKI:def 1;

               P[x, y0] by A19;

              hence thesis by A20;

            end;

          end;

          hence thesis;

        end;

        consider f2 be Function of ( Seg n), ( bool ( Seg n)) such that

         A21: for x3 be object st x3 in ( Seg n) holds P[x3, (f2 . x3)] from FUNCT_2:sch 1( A1);

        consider R be Relation of ( Seg n) such that

         A22: for i be set st i in ( Seg n) holds ( Im (R,i)) = (f2 . i) by FUNCT_2: 93;

        take R;

        let i be Element of NAT ;

        assume

         A23: i in ( Seg n);

        then ( Im (R,i)) = (f2 . i) by A22;

        hence thesis by A21, A23;

      end;

      uniqueness

      proof

        let f1,f2 be Relation of ( Seg n);

        assume that

         A24: for i be Element of NAT st i in ( Seg n) holds (1 < i & i < n implies ( Im (f1,i)) = {i, (i -' 1), (i + 1)}) & (i = 1 & i < n implies ( Im (f1,i)) = {i, n, (i + 1)}) & (1 < i & i = n implies ( Im (f1,i)) = {i, (i -' 1), 1}) & (i = 1 & i = n implies ( Im (f1,i)) = {i}) and

         A25: for i be Element of NAT st i in ( Seg n) holds (1 < i & i < n implies ( Im (f2,i)) = {i, (i -' 1), (i + 1)}) & (i = 1 & i < n implies ( Im (f2,i)) = {i, n, (i + 1)}) & (1 < i & i = n implies ( Im (f2,i)) = {i, (i -' 1), 1}) & (i = 1 & i = n implies ( Im (f2,i)) = {i});

        for x be set st x in ( Seg n) holds ( Im (f1,x)) = ( Im (f2,x))

        proof

          let x be set;

          assume

           A26: x in ( Seg n);

          then

          reconsider i2 = x as Element of NAT ;

          

           A27: 1 <= i2 & i2 <= n by A26, FINSEQ_1: 1;

          per cases by A27, XXREAL_0: 1;

            suppose

             A28: 1 < i2 & i2 < n;

            set y0 = {i2, (i2 -' 1), (i2 + 1)};

            ( Im (f1,x)) = y0 by A24, A26, A28;

            hence thesis by A25, A26, A28;

          end;

            suppose

             A29: i2 = 1 & i2 < n;

            set y0 = {i2, n, (i2 + 1)};

            ( Im (f1,x)) = y0 by A24, A26, A29;

            hence thesis by A25, A26, A29;

          end;

            suppose

             A30: 1 < i2 & i2 = n;

            set y0 = {i2, (i2 -' 1), 1};

            ( Im (f1,x)) = y0 by A24, A26, A30;

            hence thesis by A25, A26, A30;

          end;

            suppose

             A31: i2 = 1 & i2 = n;

            set y0 = {i2};

            ( Im (f1,x)) = y0 by A24, A26, A31;

            hence thesis by A25, A26, A31;

          end;

        end;

        hence f1 = f2 by RELSET_1: 31;

      end;

    end

    definition

      let n be Nat;

      assume

       A1: n > 0 ;

      :: FINTOPO4:def6

      func FTSC1 n -> non empty RelStr equals

      : Def6: RelStr (# ( Seg n), ( Nbdc1 n) #);

      correctness by A1;

    end

    theorem :: FINTOPO4:20

    for n be Element of NAT st n > 0 holds ( FTSC1 n) is filled

    proof

      let n be Element of NAT ;

      set f = ( Nbdc1 n);

      assume n > 0 ;

      then

       A1: ( FTSC1 n) = RelStr (# ( Seg n), ( Nbdc1 n) #) by Def6;

      let x be Element of ( FTSC1 n);

      x in ( Seg n) by A1;

      then

      reconsider i = x as Element of NAT ;

      

       A2: 1 <= i & i <= n by A1, FINSEQ_1: 1;

      

       A3: i = 1 & i < n implies ( Im (f,i)) = {i, n, (i + 1)} by A1, Def5;

      

       A4: 1 < i & i < n implies ( Im (f,i)) = {i, (i -' 1), (i + 1)} by A1, Def5;

      

       A5: i = 1 & i = n implies ( Im (f,i)) = {i} by A1, Def5;

      

       A6: 1 < i & i = n implies ( Im (f,i)) = {i, (i -' 1), 1} by A1, Def5;

      per cases by A2, XXREAL_0: 1;

        suppose 1 < i & i < n;

        hence thesis by A1, A4, ENUMSET1:def 1;

      end;

        suppose i = 1 & i < n;

        hence thesis by A1, A3, ENUMSET1:def 1;

      end;

        suppose 1 < i & i = n;

        hence thesis by A1, A6, ENUMSET1:def 1;

      end;

        suppose i = 1 & i = n;

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

      end;

    end;

    theorem :: FINTOPO4:21

    for n be Element of NAT st n > 0 holds ( FTSC1 n) is symmetric

    proof

      let n be Element of NAT ;

      set f = ( Nbdc1 n);

      assume n > 0 ;

      then

       A1: ( FTSC1 n) = RelStr (# ( Seg n), ( Nbdc1 n) #) by Def6;

      let x,y be Element of ( FTSC1 n);

      x in ( Seg n) by A1;

      then

      reconsider i = x as Element of NAT ;

      

       A2: 1 <= i by A1, FINSEQ_1: 1;

      

       A3: i = 1 & i < n implies ( Im (f,i)) = {i, n, (i + 1)} by A1, Def5;

      

       A4: i = 1 & i = n implies ( Im (f,i)) = {i} by A1, Def5;

      

       A5: i <= n by A1, FINSEQ_1: 1;

      y in ( Seg n) by A1;

      then

      reconsider j = y as Element of NAT ;

      

       A6: 1 <= j by A1, FINSEQ_1: 1;

      

       A7: 1 < i & i = n implies ( Im (f,i)) = {i, (i -' 1), 1} by A1, Def5;

      

       A8: 1 < i & i < n implies ( Im (f,i)) = {i, (i -' 1), (i + 1)} by A1, Def5;

      assume

       A9: y in ( U_FT x);

      

       A10: j <= n by A1, FINSEQ_1: 1;

      per cases by A2, A5, XXREAL_0: 1;

        suppose

         A11: 1 < i & i < n;

         A12:

        now

          (i - 1) > 0 by A11, XREAL_1: 50;

          then

           A13: (i -' 1) = (i - 1) by XREAL_0:def 2;

          assume

           A14: y = (i -' 1);

          per cases by A14, A13;

            suppose

             A15: x = j;

            then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, (j -' 1), (j + 1)} by A1, A11, Def5;

            hence thesis by A15, ENUMSET1:def 1;

          end;

            suppose

             A16: x = (j -' 1);

            then

             A17: i = ((i -' 1) -' 1) by A14;

            now

              assume i <> 0 ;

              then

               A18: i >= ( 0 + 1) by NAT_1: 13;

              then (i - 1) >= (1 - 1) by XREAL_1: 9;

              then

               A19: (i - 1) = (i -' 1) by XREAL_0:def 2;

              now

                assume

                 A20: i = 1;

                then ((i -' 1) - 1) < 0 by A19;

                hence contradiction by A14, A16, A20, XREAL_0:def 2;

              end;

              then i > 1 by A18, XXREAL_0: 1;

              then (i - 1) > (1 - 1) by XREAL_1: 9;

              then (i -' 1) >= ( 0 + 1) by A19, NAT_1: 13;

              then ((i -' 1) - 1) >= 0 by XREAL_1: 48;

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

              hence contradiction by A17, A19;

            end;

            hence thesis by A11;

          end;

            suppose

             A21: x = (j + 1);

            then

             A22: j < n by A5, NAT_1: 13;

             A23:

            now

              assume j <> 1;

              then j > 1 by A6, XXREAL_0: 1;

              then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, (j -' 1), (j + 1)} by A1, A22, Def5;

              hence thesis by A21, ENUMSET1:def 1;

            end;

            now

              assume j = 1;

              then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, n, (j + 1)} by A1, A22, Def5;

              hence thesis by A21, ENUMSET1:def 1;

            end;

            hence thesis by A23;

          end;

        end;

         A24:

        now

          assume

           A25: y = (i + 1);

          then

           A26: (j - 1) = x;

          now

            per cases by A11, A26, XREAL_0:def 2;

              case

               A27: x = j;

              then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, (j -' 1), (j + 1)} by A1, A11, Def5;

              hence thesis by A27, ENUMSET1:def 1;

            end;

              case

               A28: x = (j -' 1);

              now

                assume j = 1;

                then (j - 1) = 0 ;

                hence contradiction by A11, A28, XREAL_0:def 2;

              end;

              then

               A29: j > 1 by A6, XXREAL_0: 1;

               A30:

              now

                assume j <> n;

                then j < n by A10, XXREAL_0: 1;

                then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, (j -' 1), (j + 1)} by A1, A29, Def5;

                hence thesis by A28, ENUMSET1:def 1;

              end;

              now

                assume j = n;

                then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, (j -' 1), 1} by A1, A29, Def5;

                hence thesis by A28, ENUMSET1:def 1;

              end;

              hence thesis by A30;

            end;

              case x = (j + 1);

              hence contradiction by A25;

            end;

          end;

          hence thesis;

        end;

        y = i or y = (i -' 1) or y = (i + 1) by A1, A8, A9, A11, ENUMSET1:def 1;

        hence thesis by A9, A12, A24;

      end;

        suppose

         A31: i = 1 & i < n;

        per cases by A1, A3, A9, A31, ENUMSET1:def 1;

          suppose y = i & y <> n;

          hence thesis by A1, A3, A31, ENUMSET1:def 1;

        end;

          suppose y = n;

          then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, (j -' 1), 1} by A1, A31, Def5;

          hence thesis by A31, ENUMSET1:def 1;

        end;

          suppose

           A32: y = (i + 1) & y <> n;

          then (j - 1) = i;

          then

           A33: (j -' 1) = i by XREAL_0:def 2;

          j < n by A10, A32, XXREAL_0: 1;

          then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, (j -' 1), (j + 1)} by A1, A31, A32, Def5;

          hence thesis by A33, ENUMSET1:def 1;

        end;

      end;

        suppose

         A34: 1 < i & i = n;

        per cases by A1, A7, A9, A34, ENUMSET1:def 1;

          suppose y = i & y <> 1;

          hence thesis by A1, A7, A34, ENUMSET1:def 1;

        end;

          suppose y = 1;

          then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, n, (j + 1)} by A1, A34, Def5;

          hence thesis by A34, ENUMSET1:def 1;

        end;

          suppose

           A35: y = (i -' 1) & y <> 1;

          then

           A36: 1 < j by A6, XXREAL_0: 1;

          (n - 1) > 0 by A34, XREAL_1: 50;

          then

           A37: (n - 1) = (n -' 1) by XREAL_0:def 2;

          ((n - 1) + 1) = n;

          then j < n by A34, A35, A37, NAT_1: 13;

          then ( Im (the InternalRel of ( FTSC1 n),y)) = {j, (j -' 1), (j + 1)} by A1, A36, Def5;

          hence thesis by A34, A35, A37, ENUMSET1:def 1;

        end;

      end;

        suppose i = 1 & i = n;

        then j = i by A1, A4, A9, TARSKI:def 1;

        hence thesis by A9;

      end;

    end;