fintopo3.miz



    begin

    reserve T for non empty RelStr,

A,B for Subset of T,

x,x2,y,z for Element of T;

    definition

      let T;

      let A be Subset of T;

      :: FINTOPO3:def1

      func A ^d -> Subset of T equals { x where x be Element of T : for y be Element of T st y in (A ` ) holds not x in ( U_FT y) };

      coherence

      proof

        defpred P[ Element of T] means for y st y in (A ` ) holds not $1 in ( U_FT y);

        { x : P[x] } is Subset of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

    end

    theorem :: FINTOPO3:1

    

     Th1: T is filled implies A c= (A ^f )

    proof

      assume

       A1: T is filled;

      let x be object;

      assume

       A2: x in A;

      then

      reconsider y = x as Element of T;

      y in ( U_FT y) by A1, FIN_TOPO:def 4;

      hence thesis by A2, FIN_TOPO: 11;

    end;

    theorem :: FINTOPO3:2

    

     Th2: x in (A ^d ) iff for y st y in (A ` ) holds not x in ( U_FT y)

    proof

      thus x in (A ^d ) implies for y st y in (A ` ) holds not x in ( U_FT y)

      proof

        assume x in (A ^d );

        then ex y st y = x & for z st z in (A ` ) holds not y in ( U_FT z);

        hence thesis;

      end;

      assume for z st z in (A ` ) holds not x in ( U_FT z);

      hence thesis;

    end;

    theorem :: FINTOPO3:3

    

     Th3: T is filled implies (A ^d ) c= A

    proof

      assume

       A1: T is filled;

      thus (A ^d ) c= A

      proof

        let x be object;

        assume

         A2: x in (A ^d );

        then

        reconsider z = x as Element of T;

        now

          assume not x in A;

          then

           A3: x in (A ` ) by A2, SUBSET_1: 29;

          x in ( U_FT z) by A1, FIN_TOPO:def 4;

          hence contradiction by A2, A3, Th2;

        end;

        hence thesis;

      end;

    end;

    theorem :: FINTOPO3:4

    

     Th4: (A ^d ) = (((A ` ) ^f ) ` )

    proof

      for x be object holds x in (A ^d ) iff x in (((A ` ) ^f ) ` )

      proof

        let x be object;

        

         A1: ((A ` ) ^f ) = { x2 : ex y st y in (A ` ) & x2 in ( U_FT y) } by FIN_TOPO:def 12;

        thus x in (A ^d ) implies x in (((A ` ) ^f ) ` )

        proof

          

           A2: ((A ` ) ^f ) = { x2 : ex y st y in (A ` ) & x2 in ( U_FT y) } by FIN_TOPO:def 12;

          assume

           A3: x in (A ^d );

          then not (ex x2 st x2 = x & ex y st y in (A ` ) & x2 in ( U_FT y)) by Th2;

          then not x in ((A ` ) ^f ) by A2;

          hence thesis by A3, SUBSET_1: 29;

        end;

        assume

         A4: x in (((A ` ) ^f ) ` );

        then not x in ((A ` ) ^f ) by XBOOLE_0:def 5;

        then for y st y in (A ` ) holds not x in ( U_FT y) by A1;

        hence thesis by A4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINTOPO3:5

    

     Th5: A c= B implies (A ^f ) c= (B ^f )

    proof

      assume

       A1: A c= B;

      let z be object;

      assume z in (A ^f );

      then ex y st y in A & z in ( U_FT y) by FIN_TOPO: 11;

      hence thesis by A1, FIN_TOPO: 11;

    end;

    theorem :: FINTOPO3:6

    

     Th6: A c= B implies (A ^d ) c= (B ^d )

    proof

      assume A c= B;

      then

       A1: (B ` ) c= (A ` ) by SUBSET_1: 12;

      let z be object;

      assume

       A2: z in (A ^d );

      then for y st y in (B ` ) holds not z in ( U_FT y) by A1, Th2;

      hence thesis by A2;

    end;

    theorem :: FINTOPO3:7

    ((A /\ B) ^b ) c= ((A ^b ) /\ (B ^b ))

    proof

      let x be object;

      assume

       A1: x in ((A /\ B) ^b );

      then

      reconsider px = x as Point of T;

      

       A2: ( U_FT px) meets (A /\ B) by A1, FIN_TOPO: 8;

      then ( U_FT px) meets B by XBOOLE_1: 74;

      then

       A3: x in (B ^b ) by FIN_TOPO: 8;

      ( U_FT px) meets A by A2, XBOOLE_1: 74;

      then x in (A ^b ) by FIN_TOPO: 8;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    theorem :: FINTOPO3:8

    

     Th8: ((A \/ B) ^b ) = ((A ^b ) \/ (B ^b ))

    proof

      thus ((A \/ B) ^b ) c= ((A ^b ) \/ (B ^b ))

      proof

        let x be object;

        assume

         A1: x in ((A \/ B) ^b );

        then

        reconsider px = x as Point of T;

        ( U_FT px) meets (A \/ B) by A1, FIN_TOPO: 8;

        then ( U_FT px) meets A or ( U_FT px) meets B by XBOOLE_1: 70;

        then x in (A ^b ) or x in (B ^b ) by FIN_TOPO: 8;

        hence thesis by XBOOLE_0:def 3;

      end;

      let x be object;

      assume

       A2: x in ((A ^b ) \/ (B ^b ));

      then

      reconsider px = x as Point of T;

      x in (A ^b ) or x in (B ^b ) by A2, XBOOLE_0:def 3;

      then ( U_FT px) meets A or ( U_FT px) meets B by FIN_TOPO: 8;

      then ( U_FT px) meets (A \/ B) by XBOOLE_1: 70;

      hence thesis by FIN_TOPO: 8;

    end;

    theorem :: FINTOPO3:9

    ((A ^i ) \/ (B ^i )) c= ((A \/ B) ^i )

    proof

      let x be object;

      assume

       A1: x in ((A ^i ) \/ (B ^i ));

      then

      reconsider px = x as Point of T;

      x in (A ^i ) or x in (B ^i ) by A1, XBOOLE_0:def 3;

      then

       A2: ( U_FT px) c= A or ( U_FT px) c= B by FIN_TOPO: 7;

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

      then ( U_FT px) c= (A \/ B) by A2;

      hence thesis by FIN_TOPO: 7;

    end;

    theorem :: FINTOPO3:10

    

     Th10: ((A ^i ) /\ (B ^i )) = ((A /\ B) ^i )

    proof

      thus ((A ^i ) /\ (B ^i )) c= ((A /\ B) ^i )

      proof

        let x be object;

        assume

         A1: x in ((A ^i ) /\ (B ^i ));

        then

        reconsider px = x as Point of T;

        x in (B ^i ) by A1, XBOOLE_0:def 4;

        then

         A2: ( U_FT px) c= B by FIN_TOPO: 7;

        x in (A ^i ) by A1, XBOOLE_0:def 4;

        then ( U_FT px) c= A by FIN_TOPO: 7;

        then ( U_FT px) c= (A /\ B) by A2, XBOOLE_1: 19;

        hence thesis by FIN_TOPO: 7;

      end;

      let x be object;

      assume

       A3: x in ((A /\ B) ^i );

      then

      reconsider px = x as Point of T;

      

       A4: ( U_FT px) c= (A /\ B) by A3, FIN_TOPO: 7;

      then ( U_FT px) c= B by XBOOLE_1: 18;

      then

       A5: x in (B ^i ) by FIN_TOPO: 7;

      ( U_FT px) c= A by A4, XBOOLE_1: 18;

      then x in (A ^i ) by FIN_TOPO: 7;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    theorem :: FINTOPO3:11

    

     Th11: ((A ^f ) \/ (B ^f )) = ((A \/ B) ^f )

    proof

      (A ^f ) c= ((A \/ B) ^f ) & (B ^f ) c= ((A \/ B) ^f ) by Th5, XBOOLE_1: 7;

      hence ((A ^f ) \/ (B ^f )) c= ((A \/ B) ^f ) by XBOOLE_1: 8;

      let z be object;

      assume z in ((A \/ B) ^f );

      then

      consider y such that

       A1: y in (A \/ B) and

       A2: z in ( U_FT y) by FIN_TOPO: 11;

      per cases by A1, XBOOLE_0:def 3;

        suppose y in A;

        then z in (A ^f ) by A2, FIN_TOPO: 11;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose y in B;

        then z in (B ^f ) by A2, FIN_TOPO: 11;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: FINTOPO3:12

    

     Th12: ((A ^d ) /\ (B ^d )) = ((A /\ B) ^d )

    proof

      

       A1: (B ^d ) = (((B ` ) ^f ) ` ) by Th4;

      

      thus ((A ^d ) /\ (B ^d )) = ((((A ` ) ^f ) ` ) /\ (B ^d )) by Th4

      .= ((((A ` ) ^f ) \/ ((B ` ) ^f )) ` ) by A1, XBOOLE_1: 53

      .= ((((A ` ) \/ (B ` )) ^f ) ` ) by Th11

      .= ((((A /\ B) ` ) ^f ) ` ) by XBOOLE_1: 54

      .= ((A /\ B) ^d ) by Th4;

    end;

    definition

      let T be non empty RelStr;

      let A be Subset of T;

      :: FINTOPO3:def2

      func Fcl (A) -> sequence of ( bool the carrier of T) means

      : Def2: (for n be Nat, B be Subset of T st B = (it . n) holds (it . (n + 1)) = (B ^b )) & (it . 0 ) = A;

      existence

      proof

        defpred P[ set, set, set] means for B be Subset of T st B = $2 holds $3 = (B ^b );

        

         A1: for n be Nat holds for x be Subset of T holds ex y be Subset of T st P[n, x, y]

        proof

          let n be Nat, x be Subset of T;

          reconsider C = x as Subset of T;

           P[n, x, (C ^b )];

          hence thesis;

        end;

        ex f be sequence of ( bool the carrier of T) st (f . 0 ) = A & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of ( bool the carrier of T) such that

         A2: for n be Nat, B be Subset of T st B = (f1 . n) holds (f1 . (n + 1)) = (B ^b ) and

         A3: (f1 . 0 ) = A and

         A4: for n be Nat, B be Subset of T st B = (f2 . n) holds (f2 . (n + 1)) = (B ^b ) and

         A5: (f2 . 0 ) = A;

        defpred P[ Nat] means (f1 . $1) = (f2 . $1);

        

         A6: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume

           A7: P[n];

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

          reconsider B1 = (f1 . n) as Subset of T;

          (B1 ^b ) = (f1 . (n + 1)) by A2;

          hence thesis by A4, A7;

        end;

        

         A8: ( dom f1) = NAT by FUNCT_2:def 1;

        then

         A9: ( dom f1) = ( dom f2) by FUNCT_2:def 1;

        

         A10: P[ 0 ] by A3, A5;

        for n be Nat holds P[n] from NAT_1:sch 2( A10, A6);

        then for x be object st x in ( dom f1) holds (f1 . x) = (f2 . x) by A8;

        hence f1 = f2 by A9, FUNCT_1: 2;

      end;

    end

    definition

      let T be non empty RelStr;

      let A be Subset of T, n be Nat;

      :: FINTOPO3:def3

      func Fcl (A,n) -> Subset of T equals (( Fcl A) . n);

      coherence

      proof

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        (( Fcl A) . n9) c= the carrier of T;

        hence thesis;

      end;

    end

    definition

      let T be non empty RelStr;

      let A be Subset of T;

      :: FINTOPO3:def4

      func Fint (A) -> sequence of ( bool the carrier of T) means

      : Def4: (for n be Nat, B be Subset of T st B = (it . n) holds (it . (n + 1)) = (B ^i )) & (it . 0 ) = A;

      existence

      proof

        defpred P[ set, set, set] means for B be Subset of T st B = $2 holds $3 = (B ^i );

        

         A1: for n be Nat holds for x be Subset of T holds ex y be Subset of T st P[n, x, y]

        proof

          let n be Nat, x be Subset of T;

          reconsider C = x as Subset of T;

          for B be Subset of T st B = x holds (C ^i ) = (B ^i );

          hence thesis;

        end;

        ex f be sequence of ( bool the carrier of T) st (f . 0 ) = A & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of ( bool the carrier of T) such that

         A2: for n be Nat, B be Subset of T st B = (f1 . n) holds (f1 . (n + 1)) = (B ^i ) and

         A3: (f1 . 0 ) = A and

         A4: for n be Nat, B be Subset of T st B = (f2 . n) holds (f2 . (n + 1)) = (B ^i ) and

         A5: (f2 . 0 ) = A;

        defpred P[ Nat] means (f1 . $1) = (f2 . $1);

        

         A6: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume

           A7: P[n];

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

          reconsider B1 = (f1 . n) as Subset of T;

          (B1 ^i ) = (f1 . (n + 1)) by A2;

          hence thesis by A4, A7;

        end;

        

         A8: ( dom f1) = NAT by FUNCT_2:def 1;

        then

         A9: ( dom f1) = ( dom f2) by FUNCT_2:def 1;

        

         A10: P[ 0 ] by A3, A5;

        for n be Nat holds P[n] from NAT_1:sch 2( A10, A6);

        then for x be object st x in ( dom f1) holds (f1 . x) = (f2 . x) by A8;

        hence f1 = f2 by A9, FUNCT_1: 2;

      end;

    end

    definition

      let T be non empty RelStr;

      let A be Subset of T, n be Nat;

      :: FINTOPO3:def5

      func Fint (A,n) -> Subset of T equals (( Fint A) . n);

      coherence

      proof

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        (( Fint A) . n9) c= the carrier of T;

        hence thesis;

      end;

    end

    theorem :: FINTOPO3:13

    for n be Nat holds ( Fcl (A,(n + 1))) = (( Fcl (A,n)) ^b ) by Def2;

    theorem :: FINTOPO3:14

    ( Fcl (A, 0 )) = A by Def2;

    theorem :: FINTOPO3:15

    

     Th15: ( Fcl (A,1)) = (A ^b )

    proof

      (( Fcl A) . 0 ) = A by Def2;

      then (( Fcl A) . ( 0 + 1)) = (A ^b ) by Def2;

      hence thesis;

    end;

    theorem :: FINTOPO3:16

    ( Fcl (A,2)) = ((A ^b ) ^b )

    proof

      for B be Subset of T st B = (( Fcl A) . 1) holds (( Fcl A) . (1 + 1)) = (B ^b ) by Def2;

      

      then ( Fcl (A,2)) = (( Fcl (A,1)) ^b )

      .= ((A ^b ) ^b ) by Th15;

      hence thesis;

    end;

    theorem :: FINTOPO3:17

    

     Th17: for n be Nat holds ( Fcl ((A \/ B),n)) = (( Fcl (A,n)) \/ ( Fcl (B,n)))

    proof

      let n be Nat;

      for n be Nat holds (( Fcl (A \/ B)) . n) = ((( Fcl A) . n) \/ (( Fcl B) . n))

      proof

        defpred P[ Nat] means (( Fcl (A \/ B)) . $1) = ((( Fcl A) . $1) \/ (( Fcl B) . $1));

        

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

        proof

          let k be Nat;

          assume

           A2: P[k];

          (( Fcl (A \/ B)) . (k + 1)) = (( Fcl ((A \/ B),k)) ^b ) by Def2

          .= ((( Fcl (A,k)) ^b ) \/ (( Fcl (B,k)) ^b )) by A2, Th8

          .= (( Fcl (A,(k + 1))) \/ (( Fcl (B,k)) ^b )) by Def2

          .= ((( Fcl A) . (k + 1)) \/ (( Fcl B) . (k + 1))) by Def2;

          hence thesis;

        end;

        (( Fcl (A \/ B)) . 0 ) = (A \/ B) by Def2

        .= ((( Fcl A) . 0 ) \/ B) by Def2

        .= ((( Fcl A) . 0 ) \/ (( Fcl B) . 0 )) by Def2;

        then

         A3: P[ 0 ];

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

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO3:18

    for n be Nat holds ( Fint (A,(n + 1))) = (( Fint (A,n)) ^i ) by Def4;

    theorem :: FINTOPO3:19

    ( Fint (A, 0 )) = A by Def4;

    theorem :: FINTOPO3:20

    

     Th20: ( Fint (A,1)) = (A ^i )

    proof

      (( Fint A) . 0 ) = A & for B be Subset of T st B = (( Fint A) . 0 ) holds (( Fint A) . ( 0 + 1)) = (B ^i ) by Def4;

      hence thesis;

    end;

    theorem :: FINTOPO3:21

    ( Fint (A,2)) = ((A ^i ) ^i )

    proof

      

      thus ( Fint (A,2)) = ( Fint (A,(1 + 1)))

      .= (( Fint (A,1)) ^i ) by Def4

      .= ((A ^i ) ^i ) by Th20;

    end;

    theorem :: FINTOPO3:22

    

     Th22: for n be Nat holds ( Fint ((A /\ B),n)) = (( Fint (A,n)) /\ ( Fint (B,n)))

    proof

      defpred P[ Nat] means (( Fint (A /\ B)) . $1) = ((( Fint A) . $1) /\ (( Fint B) . $1));

      let n be Nat;

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        (( Fint (A /\ B)) . (k + 1)) = (( Fint ((A /\ B),k)) ^i ) by Def4

        .= ((( Fint (A,k)) ^i ) /\ (( Fint (B,k)) ^i )) by A2, Th10

        .= (( Fint (A,(k + 1))) /\ (( Fint (B,k)) ^i )) by Def4

        .= ((( Fint A) . (k + 1)) /\ (( Fint B) . (k + 1))) by Def4;

        hence thesis;

      end;

      (( Fint (A /\ B)) . 0 ) = (A /\ B) by Def4

      .= ((( Fint A) . 0 ) /\ B) by Def4

      .= ((( Fint A) . 0 ) /\ (( Fint B) . 0 )) by Def4;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FINTOPO3:23

    T is filled implies for n be Nat holds A c= ( Fcl (A,n))

    proof

      defpred P[ Nat] means A c= (( Fcl A) . $1);

      assume

       A1: T is filled;

      

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

      proof

        let k be Nat;

        assume P[k];

        then (A ^b ) c= (( Fcl (A,k)) ^b ) by FIN_TOPO: 14;

        then

         A3: (A ^b ) c= ( Fcl (A,(k + 1))) by Def2;

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

        hence thesis by A3, XBOOLE_1: 1;

      end;

      let n be Nat;

      

       A4: P[ 0 ] by Def2;

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

      hence thesis;

    end;

    theorem :: FINTOPO3:24

    T is filled implies for n be Nat holds ( Fint (A,n)) c= A

    proof

      defpred P[ Nat] means (( Fint A) . $1) c= A;

      assume

       A1: T is filled;

      

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

      proof

        let k be Nat;

        assume P[k];

        then (( Fint (A,k)) ^i ) c= (A ^i ) by FINTOPO2: 1;

        then

         A3: ( Fint (A,(k + 1))) c= (A ^i ) by Def4;

        (A ^i ) c= A by A1, FIN_TOPO: 22;

        hence thesis by A3, XBOOLE_1: 1;

      end;

      let n be Nat;

      

       A4: P[ 0 ] by Def4;

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

      hence thesis;

    end;

    theorem :: FINTOPO3:25

    T is filled implies for n be Nat holds ( Fcl (A,n)) c= ( Fcl (A,(n + 1)))

    proof

      assume

       A1: T is filled;

      let n be Nat;

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

      ((( Fcl A) . n) ^b ) = ( Fcl (A,(n + 1))) by Def2;

      hence thesis by A1, FIN_TOPO: 13;

    end;

    theorem :: FINTOPO3:26

    T is filled implies for n be Nat holds ( Fint (A,(n + 1))) c= ( Fint (A,n))

    proof

      assume

       A1: T is filled;

      let n be Nat;

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

      ((( Fint A) . n) ^i ) = ( Fint (A,(n + 1))) by Def4;

      hence thesis by A1, FIN_TOPO: 22;

    end;

    theorem :: FINTOPO3:27

    

     Th27: for n be Nat holds (( Fint ((A ` ),n)) ` ) = ( Fcl (A,n))

    proof

      defpred P[ Nat] means (( Fint ((A ` ),$1)) ` ) = ( Fcl (A,$1));

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        ( Fcl (A,(k + 1))) = (( Fcl (A,k)) ^b ) by Def2

        .= ((((( Fint ((A ` ),k)) ` ) ` ) ^i ) ` ) by A2, FIN_TOPO: 16

        .= (( Fint ((A ` ),(k + 1))) ` ) by Def4;

        hence thesis;

      end;

      (( Fint ((A ` ), 0 )) ` ) = ((A ` ) ` ) by Def4

      .= ( Fcl (A, 0 )) by Def2;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FINTOPO3:28

    

     Th28: for n be Nat holds (( Fcl ((A ` ),n)) ` ) = ( Fint (A,n))

    proof

      let n be Nat;

      ( Fint (A,n)) = ((( Fint (((A ` ) ` ),n)) ` ) ` )

      .= (( Fcl ((A ` ),n)) ` ) by Th27;

      hence thesis;

    end;

    theorem :: FINTOPO3:29

    for n be Nat holds (( Fcl (A,n)) \/ ( Fcl (B,n))) = (( Fint (((A \/ B) ` ),n)) ` )

    proof

      let n be Nat;

      (( Fcl (A,n)) \/ ( Fcl (B,n))) = ( Fcl ((A \/ B),n)) by Th17

      .= (( Fint (((A \/ B) ` ),n)) ` ) by Th27;

      hence thesis;

    end;

    theorem :: FINTOPO3:30

    for n be Nat holds (( Fint (A,n)) /\ ( Fint (B,n))) = (( Fcl (((A /\ B) ` ),n)) ` )

    proof

      let n be Nat;

      (( Fint (A,n)) /\ ( Fint (B,n))) = ( Fint ((A /\ B),n)) by Th22

      .= (( Fcl (((A /\ B) ` ),n)) ` ) by Th28;

      hence thesis;

    end;

    definition

      let T be non empty RelStr;

      let A be Subset of T;

      :: FINTOPO3:def6

      func Finf (A) -> sequence of ( bool the carrier of T) means

      : Def6: (for n be Nat, B be Subset of T st B = (it . n) holds (it . (n + 1)) = (B ^f )) & (it . 0 ) = A;

      existence

      proof

        defpred P[ set, set, set] means (for B be Subset of T st B = $2 holds $3 = (B ^f ));

        

         A1: for n be Nat holds for x be Subset of T holds ex y be Subset of T st P[n, x, y]

        proof

          let n be Nat, x be Subset of T;

          reconsider C = x as Subset of T;

          for B be Subset of T st B = x holds (C ^f ) = (B ^f );

          hence thesis;

        end;

        ex f be sequence of ( bool the carrier of T) st (f . 0 ) = A & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of ( bool the carrier of T) such that

         A2: for n be Nat, B be Subset of T st B = (f1 . n) holds (f1 . (n + 1)) = (B ^f ) and

         A3: (f1 . 0 ) = A and

         A4: for n be Nat, B be Subset of T st B = (f2 . n) holds (f2 . (n + 1)) = (B ^f ) and

         A5: (f2 . 0 ) = A;

        defpred P[ Nat] means (f1 . $1) = (f2 . $1);

        

         A6: ( dom f1) = NAT by FUNCT_2:def 1;

        then

         A7: ( dom f1) = ( dom f2) by FUNCT_2:def 1;

        for n be Nat holds P[n]

        proof

          let n be Nat;

          

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

          proof

            let k be Nat;

            assume

             A9: P[k];

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

            reconsider B1 = (f1 . k) as Subset of T;

            (B1 ^f ) = (f1 . (k + 1)) by A2;

            hence thesis by A4, A9;

          end;

          

           A10: P[ 0 ] by A3, A5;

          for m be Nat holds P[m] from NAT_1:sch 2( A10, A8);

          hence thesis;

        end;

        then for x be object st x in ( dom f1) holds (f1 . x) = (f2 . x) by A6;

        hence f1 = f2 by A7, FUNCT_1: 2;

      end;

    end

    definition

      let T be non empty RelStr;

      let A be Subset of T, n be Nat;

      :: FINTOPO3:def7

      func Finf (A,n) -> Subset of T equals (( Finf A) . n);

      coherence

      proof

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        (( Finf A) . n9) c= the carrier of T;

        hence thesis;

      end;

    end

    definition

      let T be non empty RelStr;

      let A be Subset of T;

      :: FINTOPO3:def8

      func Fdfl (A) -> sequence of ( bool the carrier of T) means

      : Def8: (for n be Nat, B be Subset of T st B = (it . n) holds (it . (n + 1)) = (B ^d )) & (it . 0 ) = A;

      existence

      proof

        defpred P[ set, set, set] means for B be Subset of T st B = $2 holds $3 = (B ^d );

        

         A1: for n be Nat holds for x be Subset of T holds ex y be Subset of T st P[n, x, y]

        proof

          let n be Nat, x be Subset of T;

          for B be Subset of T st B = x holds (x ^d ) = (B ^d );

          hence thesis;

        end;

        ex f be sequence of ( bool the carrier of T) st (f . 0 ) = A & for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of ( bool the carrier of T) such that

         A2: for n be Nat, B be Subset of T st B = (f1 . n) holds (f1 . (n + 1)) = (B ^d ) and

         A3: (f1 . 0 ) = A and

         A4: for n be Nat, B be Subset of T st B = (f2 . n) holds (f2 . (n + 1)) = (B ^d ) and

         A5: (f2 . 0 ) = A;

        defpred P[ Nat] means (f1 . $1) = (f2 . $1);

        

         A6: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume

           A7: P[n];

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

          reconsider B1 = (f1 . n) as Subset of T;

          (B1 ^d ) = (f1 . (n + 1)) by A2;

          hence thesis by A4, A7;

        end;

        

         A8: ( dom f1) = NAT by FUNCT_2:def 1;

        then

         A9: ( dom f1) = ( dom f2) by FUNCT_2:def 1;

        

         A10: P[ 0 ] by A3, A5;

        for n be Nat holds P[n] from NAT_1:sch 2( A10, A6);

        then for x be object st x in ( dom f1) holds (f1 . x) = (f2 . x) by A8;

        hence f1 = f2 by A9, FUNCT_1: 2;

      end;

    end

    definition

      let T be non empty RelStr;

      let A be Subset of T, n be Nat;

      :: FINTOPO3:def9

      func Fdfl (A,n) -> Subset of T equals (( Fdfl A) . n);

      coherence

      proof

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        (( Fdfl A) . n9) c= the carrier of T;

        hence thesis;

      end;

    end

    theorem :: FINTOPO3:31

    for n be Nat holds ( Finf (A,(n + 1))) = (( Finf (A,n)) ^f ) by Def6;

    theorem :: FINTOPO3:32

    ( Finf (A, 0 )) = A by Def6;

    theorem :: FINTOPO3:33

    

     Th33: ( Finf (A,1)) = (A ^f )

    proof

      (( Finf A) . 0 ) = A & for B be Subset of T st B = (( Finf A) . 0 ) holds (( Finf A) . ( 0 + 1)) = (B ^f ) by Def6;

      hence thesis;

    end;

    theorem :: FINTOPO3:34

    ( Finf (A,2)) = ((A ^f ) ^f )

    proof

      ( Finf (A,2)) = ( Finf (A,(1 + 1)))

      .= (( Finf (A,1)) ^f ) by Def6

      .= ((A ^f ) ^f ) by Th33;

      hence thesis;

    end;

    theorem :: FINTOPO3:35

    for n be Nat holds ( Finf ((A \/ B),n)) = (( Finf (A,n)) \/ ( Finf (B,n)))

    proof

      defpred P[ Nat] means (( Finf (A \/ B)) . $1) = ((( Finf A) . $1) \/ (( Finf B) . $1));

      let n be Nat;

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        (( Finf (A \/ B)) . (k + 1)) = (( Finf ((A \/ B),k)) ^f ) by Def6

        .= ((( Finf (A,k)) ^f ) \/ (( Finf (B,k)) ^f )) by A2, Th11

        .= (( Finf (A,(k + 1))) \/ (( Finf (B,k)) ^f )) by Def6

        .= ((( Finf A) . (k + 1)) \/ (( Finf B) . (k + 1))) by Def6;

        hence thesis;

      end;

      (( Finf (A \/ B)) . 0 ) = (A \/ B) by Def6

      .= ((( Finf A) . 0 ) \/ B) by Def6

      .= ((( Finf A) . 0 ) \/ (( Finf B) . 0 )) by Def6;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FINTOPO3:36

    T is filled implies for n be Nat holds A c= ( Finf (A,n))

    proof

      defpred P[ Nat] means A c= (( Finf A) . $1);

      assume

       A1: T is filled;

      

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

      proof

        let k be Nat;

        assume P[k];

        then (A ^f ) c= (( Finf (A,k)) ^f ) by Th5;

        then

         A3: (A ^f ) c= ( Finf (A,(k + 1))) by Def6;

        A c= (A ^f ) by A1, Th1;

        hence thesis by A3, XBOOLE_1: 1;

      end;

      let n be Nat;

      

       A4: P[ 0 ] by Def6;

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

      hence thesis;

    end;

    theorem :: FINTOPO3:37

    T is filled implies for n be Nat holds ( Finf (A,n)) c= ( Finf (A,(n + 1)))

    proof

      assume

       A1: T is filled;

      let n be Nat;

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

      ((( Finf A) . n) ^f ) = ( Finf (A,(n + 1))) by Def6;

      hence thesis by A1, Th1;

    end;

    theorem :: FINTOPO3:38

    for n be Nat holds ( Fdfl (A,(n + 1))) = (( Fdfl (A,n)) ^d ) by Def8;

    theorem :: FINTOPO3:39

    ( Fdfl (A, 0 )) = A by Def8;

    theorem :: FINTOPO3:40

    

     Th40: ( Fdfl (A,1)) = (A ^d )

    proof

      (( Fdfl A) . 0 ) = A & for B be Subset of T st B = (( Fdfl A) . 0 ) holds (( Fdfl A) . ( 0 + 1)) = (B ^d ) by Def8;

      hence thesis;

    end;

    theorem :: FINTOPO3:41

    ( Fdfl (A,2)) = ((A ^d ) ^d )

    proof

      ( Fdfl (A,2)) = ( Fdfl (A,(1 + 1)))

      .= (( Fdfl (A,1)) ^d ) by Def8;

      hence thesis by Th40;

    end;

    theorem :: FINTOPO3:42

    

     Th42: for n be Nat holds ( Fdfl ((A /\ B),n)) = (( Fdfl (A,n)) /\ ( Fdfl (B,n)))

    proof

      defpred P[ Nat] means (( Fdfl (A /\ B)) . $1) = ((( Fdfl A) . $1) /\ (( Fdfl B) . $1));

      let n be Nat;

      

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

      proof

        let k be Nat;

        assume

         A2: P[k];

        (( Fdfl (A /\ B)) . (k + 1)) = (( Fdfl ((A /\ B),k)) ^d ) by Def8

        .= ((( Fdfl (A,k)) ^d ) /\ (( Fdfl (B,k)) ^d )) by A2, Th12

        .= (( Fdfl (A,(k + 1))) /\ (( Fdfl (B,k)) ^d )) by Def8

        .= ((( Fdfl A) . (k + 1)) /\ (( Fdfl B) . (k + 1))) by Def8;

        hence thesis;

      end;

      (( Fdfl (A /\ B)) . 0 ) = (A /\ B) by Def8

      .= ((( Fdfl A) . 0 ) /\ B) by Def8

      .= ((( Fdfl A) . 0 ) /\ (( Fdfl B) . 0 )) by Def8;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FINTOPO3:43

    T is filled implies for n be Nat holds ( Fdfl (A,n)) c= A

    proof

      defpred P[ Nat] means (( Fdfl A) . $1) c= A;

      assume

       A1: T is filled;

      

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

      proof

        let k be Nat;

        assume P[k];

        then (( Fdfl (A,k)) ^d ) c= (A ^d ) by Th6;

        then

         A3: ( Fdfl (A,(k + 1))) c= (A ^d ) by Def8;

        (A ^d ) c= A by A1, Th3;

        hence thesis by A3, XBOOLE_1: 1;

      end;

      let n be Nat;

      

       A4: P[ 0 ] by Def8;

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

      hence thesis;

    end;

    theorem :: FINTOPO3:44

    T is filled implies for n be Nat holds ( Fdfl (A,(n + 1))) c= ( Fdfl (A,n))

    proof

      assume

       A1: T is filled;

      let n be Nat;

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

      ((( Fdfl A) . n) ^d ) = ( Fdfl (A,(n + 1))) by Def8;

      hence thesis by A1, Th3;

    end;

    theorem :: FINTOPO3:45

    

     Th45: for n be Nat holds ( Fdfl (A,n)) = (( Finf ((A ` ),n)) ` )

    proof

      defpred P[ Nat] means (( Fdfl A) . $1) = ((( Finf (A ` )) . ( In ($1, NAT ))) ` );

      let n be Nat;

      

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

      proof

        let k be Nat;

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

        assume

         A2: P[k];

        (( Fdfl A) . (k + 1)) = (( Fdfl (A,k)) ^d ) by Def8;

        

        then (( Fdfl A) . (k + 1)) = ((((( Fdfl A) . kk) ` ) ^f ) ` ) by Th4

        .= ((( Finf (A ` )) . ( In ((k + 1), NAT ))) ` ) by A2, Def6;

        hence thesis;

      end;

      ((( Finf (A ` )) . 0 ) ` ) = ((A ` ) ` ) by Def6

      .= A;

      then

       A3: P[ 0 ] by Def8;

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

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

      then P[n];

      hence thesis;

    end;

    theorem :: FINTOPO3:46

    for n be Nat holds (( Fdfl (A,n)) /\ ( Fdfl (B,n))) = (( Finf (((A /\ B) ` ),n)) ` )

    proof

      let n be Nat;

      (( Fdfl (A,n)) /\ ( Fdfl (B,n))) = ( Fdfl ((A /\ B),n)) by Th42

      .= (( Finf (((A /\ B) ` ),n)) ` ) by Th45;

      hence thesis;

    end;

    definition

      let T be non empty RelStr, n be Nat, x be Element of T;

      :: FINTOPO3:def10

      func U_FT (x,n) -> Subset of T equals ( Finf (( U_FT x),n));

      coherence ;

    end

    theorem :: FINTOPO3:47

    ( U_FT (x, 0 )) = ( U_FT x) by Def6;

    theorem :: FINTOPO3:48

    for n be Nat holds ( U_FT (x,(n + 1))) = (( U_FT (x,n)) ^f ) by Def6;

    definition

      let S,T be non empty RelStr;

      :: FINTOPO3:def11

      pred S,T are_mutually_symmetric means the carrier of S = the carrier of T & for x be Element of S, y be Element of T holds y in ( U_FT x) iff x in ( U_FT y);

      symmetry ;

    end