fin_topo.miz



    begin

    theorem :: FIN_TOPO:1

    

     Th1: for A be set, f be FinSequence of ( bool A) st (for i be Nat st 1 <= i & i < ( len f) holds (f /. i) c= (f /. (i + 1))) holds for i,j be Nat st i <= j & 1 <= i & j <= ( len f) holds (f /. i) c= (f /. j)

    proof

      let A be set;

      let f be FinSequence of ( bool A) such that

       A1: for i be Nat st 1 <= i & i < ( len f) holds (f /. i) c= (f /. (i + 1));

      let i,j be Nat such that

       A2: i <= j and

       A3: 1 <= i and

       A4: j <= ( len f);

      consider k be Nat such that

       A5: (i + k) = j by A2, NAT_1: 10;

      defpred P[ Nat] means (i + $1) <= j implies (f /. i) c= (f /. (i + $1));

       A6:

      now

        let k be Nat;

        

         A7: ((i + k) + 1) = (i + (k + 1));

        assume

         A8: P[k];

        thus P[(k + 1)]

        proof

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

          then

           A9: (i + k) >= 1 by A3, XXREAL_0: 2;

          assume

           A10: (i + (k + 1)) <= j;

          then (i + k) < j by A7, NAT_1: 13;

          then (i + k) < ( len f) by A4, XXREAL_0: 2;

          then (f /. (i + k)) c= (f /. (i + (k + 1))) by A1, A7, A9;

          hence thesis by A7, A8, A10, NAT_1: 13;

        end;

      end;

      

       A11: P[ 0 ];

      

       A12: for k be Nat holds P[k] from NAT_1:sch 2( A11, A6);

      thus thesis by A12, A5;

    end;

    theorem :: FIN_TOPO:2

    

     Th2: for A be set, f be FinSequence of ( bool A) st (for i be Nat st 1 <= i & i < ( len f) holds (f /. i) c= (f /. (i + 1))) holds for i,j be Nat st 1 <= i & j <= ( len f) & (f /. j) c= (f /. i) holds for k be Nat st i <= k <= j holds (f /. j) = (f /. k)

    proof

      let A be set;

      let f be FinSequence of ( bool A) such that

       A1: for i be Nat st 1 <= i < ( len f) holds (f /. i) c= (f /. (i + 1));

      let i,j be Nat;

      assume that

       A2: 1 <= i and

       A3: j <= ( len f) and

       A4: (f /. j) c= (f /. i);

      let k be Nat;

      assume that

       A5: i <= k and

       A6: k <= j;

      1 <= k by A2, A5, XXREAL_0: 2;

      then

       A7: (f /. k) c= (f /. j) by A1, A3, A6, Th1;

      defpred P[ Nat] means (i + $1) <= j implies (f /. j) c= (f /. (i + $1));

       A8:

      now

        let k be Nat;

        assume

         A9: P[k];

        

         A10: ((i + k) + 1) = (i + (k + 1));

        thus P[(k + 1)]

        proof

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

          then

           A11: (i + k) >= 1 by A2, XXREAL_0: 2;

          assume

           A12: (i + (k + 1)) <= j;

          then (i + k) < j by A10, NAT_1: 13;

          then (i + k) < ( len f) by A3, XXREAL_0: 2;

          then (f /. (i + k)) c= (f /. ((i + k) + 1)) by A1, A11;

          hence thesis by A9, A12, NAT_1: 13;

        end;

      end;

      

       A13: P[ 0 ] by A4;

      

       A14: for k be Nat holds P[k] from NAT_1:sch 2( A13, A8);

      consider m be Nat such that

       A15: k = (i + m) by A5, NAT_1: 10;

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

      k = (i + m) by A15;

      then (f /. j) c= (f /. k) by A14, A6;

      hence thesis by A7;

    end;

    scheme :: FIN_TOPO:sch1

    MaxFinSeqEx { X() -> non empty set , A,B() -> Subset of X() , F( Subset of X()) -> Subset of X() } :

ex f be FinSequence of ( bool X()) st ( len f) > 0 & (f /. 1) = B() & (for i be Nat st i > 0 & i < ( len f) holds (f /. (i + 1)) = F(/.)) & F(/.) = (f /. ( len f)) & for i,j be Nat st i > 0 & i < j & j <= ( len f) holds (f /. i) c= A() & (f /. i) c< (f /. j)

      provided

       A1: A() is finite

       and

       A2: B() c= A()

       and

       A3: for A be Subset of X() st A c= A() holds A c= F(A) & F(A) c= A();

      deffunc F( Nat, Subset of X()) = F($2);

      consider f be sequence of ( bool X()) such that

       A4: (f . 0 ) = B() and

       A5: for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 12;

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

       A6:

      now

        let n be Nat such that

         A7: P[n];

        (f . (n + 1)) = F(.) by A5;

        hence P[(n + 1)] by A3, A7;

      end;

      

       A8: P[ 0 ] by A2, A4;

      

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

      

       A10: for i be Nat holds (f . i) c= (f . (i + 1))

      proof

        let i be Nat;

        (f . (i + 1)) = F(.) & (f . i) c= A() by A5, A9;

        hence thesis by A3;

      end;

      

       A11: ( dom f) = NAT by FUNCT_2:def 1;

      

       A12: ( rng f) is c=-linear

      proof

        let B,C be set;

        assume B in ( rng f);

        then

        consider i be object such that

         A13: i in NAT and

         A14: B = (f . i) by A11, FUNCT_1:def 3;

        reconsider i as Element of NAT by A13;

        assume C in ( rng f);

        then

        consider j be object such that

         A15: j in NAT and

         A16: C = (f . j) by A11, FUNCT_1:def 3;

        reconsider j as Element of NAT by A15;

        i <= j or j <= i;

        hence B c= C or C c= B by A10, A14, A16, MEASURE2: 18;

      end;

      

       A17: ( rng f) c= ( bool A())

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in ( rng f);

        then x in (f .: NAT ) by RELSET_1: 22;

        then ex k be Element of NAT st k in NAT & (f . k) = x by FUNCT_2: 65;

        then xx c= A() by A9;

        hence thesis;

      end;

      ( rng f) <> {} by A4, A11, FUNCT_1:def 3;

      then

      consider m be set such that

       A18: m in ( rng f) and

       A19: for C be set st C in ( rng f) holds C c= m by A1, A17, A12, FINSET_1: 12;

      deffunc G( Nat) = (f . |.($1 - 1).|);

      defpred P[ set] means $1 in NAT & (f . $1) = m;

      m in (f .: NAT ) by A18, RELSET_1: 22;

      then ex k be Element of NAT st P[k] by FUNCT_2: 65;

      then

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

      consider k be Nat such that

       A21: P[k] and

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

      consider z be FinSequence of ( bool X()) such that

       A23: ( len z) = (k + 1) and

       A24: for j be Nat st j in ( dom z) holds (z . j) = G(j) from FINSEQ_2:sch 1;

      

       A25: ( 0 + 1) <= ( len z) by A23, NAT_1: 13;

      then

       A26: 1 in ( Seg (k + 1)) by A23, FINSEQ_1: 1;

      take z;

      thus 0 < ( len z) by A23;

      

       A27: ( dom z) = ( Seg (k + 1)) by A23, FINSEQ_1:def 3;

      

      thus (z /. 1) = (z . 1) by A25, FINSEQ_4: 15

      .= (f . |.(1 - 1).|) by A24, A27, A26

      .= B() by A4, ABSVALUE: 2;

      thus

       A28: for i be Nat st i > 0 & i < ( len z) holds (z /. (i + 1)) = F(/.)

      proof

        let i be Nat;

        assume that

         A29: i > 0 and

         A30: i < ( len z);

        

         A31: ( 0 + 1) < (i + 1) & (i + 1) <= (k + 1) by A23, A29, A30, NAT_1: 13, XREAL_1: 6;

        then

         A32: (i + 1) in ( Seg (k + 1)) by FINSEQ_1: 1;

        

         A33: ( 0 + 1) <= i by A29, NAT_1: 13;

        then i in ( Seg (k + 1)) by A23, A30, FINSEQ_1: 1;

        then

         A34: (z . i) = (f . |.(i - 1).|) & i in ( dom z) by A24, A27;

        (1 - 1) <= (i - 1) by A33, XREAL_1: 9;

        then

         A35: 0 <= ((i - 1) * 1);

        

        thus (z /. (i + 1)) = (z . (i + 1)) by A23, A31, FINSEQ_4: 15

        .= (f . |.((i + 1) - 1).|) by A24, A27, A32

        .= (f . |.((i - 1) + 1).|)

        .= (f . ( |.(i - 1).| + |.1.|)) by A35, ABSVALUE: 11

        .= (f . ( |.(i - 1).| + 1)) by ABSVALUE:def 1

        .= F(.) by A5

        .= F(/.) by A34, PARTFUN1:def 6;

      end;

      thus F(/.) = (z /. ( len z))

      proof

        (k + 1) in NAT ;

        then (k + 1) in ( dom f) by FUNCT_2:def 1;

        then (f . (k + 1)) in ( rng f) by FUNCT_1:def 3;

        then

         A36: (f . (k + 1)) c= (f . k) by A19, A21;

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

        

         A37: (f . k) c= (f . (k + 1)) by A10;

        ( len z) = 0 or ( len z) in ( Seg ( len z)) by FINSEQ_1: 3;

        then

         A38: ( len z) in ( dom z) by A23, FINSEQ_1:def 3;

        

         A39: (z . ( len z)) = (f . |.((k + 1) - 1).|) by A23, A24, A27, FINSEQ_1: 3

        .= (f . k) by ABSVALUE:def 1;

        

        hence F(/.) = F(.) by A38, PARTFUN1:def 6

        .= (f . (k + 1)) by A5

        .= (z . ( len z)) by A37, A36, A39

        .= (z /. ( len z)) by A38, PARTFUN1:def 6;

      end;

      let i,j be Nat;

      assume that

       A40: 0 < i and

       A41: i < j and

       A42: j <= ( len z);

      

       A43: ( 0 + 1) <= i by A40, NAT_1: 13;

      then

      reconsider l = (i - 1) as Element of NAT by INT_1: 5;

      

       A44: i <= ( len z) by A41, A42, XXREAL_0: 2;

      then

       A45: i in ( Seg (k + 1)) by A23, A43, FINSEQ_1: 1;

      

       A46: (z /. i) = (z . i) by A43, A44, FINSEQ_4: 15

      .= (f . |.(i - 1).|) by A24, A27, A45

      .= (f . l) by ABSVALUE:def 1;

      hence (z /. i) c= A() by A9;

      

       A47: for i be Nat st 1 <= i & i < ( len z) holds (z /. i) c= (z /. (i + 1))

      proof

        let i be Nat;

        assume that

         A48: 1 <= i and

         A49: i < ( len z);

        

         A50: i in ( Seg (k + 1)) by A23, A48, A49, FINSEQ_1: 1;

        

         A51: (1 - 1) <= (i - 1) by A48, XREAL_1: 9;

        then

         A52: (i - 1) is Element of NAT by INT_1: 3;

        

         A53: 1 <= (i + 1) & (i + 1) <= ( len z) by A48, A49, NAT_1: 13;

        then

         A54: (i + 1) in ( Seg (k + 1)) by A23, FINSEQ_1: 1;

        

         A55: (z /. (i + 1)) = (z . (i + 1)) by A53, FINSEQ_4: 15

        .= (f . |.((i + 1) - 1).|) by A24, A27, A54

        .= (f . ((i - 1) + 1)) by ABSVALUE:def 1;

        (z /. i) = (z . i) by A48, A49, FINSEQ_4: 15

        .= (f . |.(i - 1).|) by A24, A27, A50

        .= (f . (i - 1)) by A51, ABSVALUE:def 1;

        hence thesis by A10, A55, A52;

      end;

      hence (z /. i) c= (z /. j) by A41, A42, A43, Th1;

      defpred P[ Nat] means (i + $1) <= ( len z) implies (z /. i) = (z /. (i + $1));

      

       A56: i <= (i + 1) & (i + 1) <= j by A41, NAT_1: 13;

      (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

      then

       A57: (k + 1) in ( dom z) by A23, FINSEQ_1:def 3;

      

       A58: i < ( len z) by A41, A42, XXREAL_0: 2;

      assume (z /. i) = (z /. j);

      

      then

       A59: (z /. i) = (z /. (i + 1)) by A42, A43, A47, A56, Th2

      .= F(/.) by A28, A40, A58;

       A60:

      now

        let n be Nat such that

         A61: P[n];

        thus P[(n + 1)]

        proof

          assume (i + (n + 1)) <= ( len z);

          then ((i + n) + 1) <= ( len z);

          then (i + n) < ( len z) by NAT_1: 13;

          

          hence (z /. i) = (z /. ((i + n) + 1)) by A28, A40, A59, A61

          .= (z /. (i + (n + 1)));

        end;

      end;

      consider n0 be Nat such that

       A62: (i + n0) = ( len z) by A41, A42, NAT_1: 10, XXREAL_0: 2;

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

      

       A63: (i + n0) = ( len z) by A62;

      

       A64: P[ 0 ];

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

      

      then (f . l) = (z /. (k + 1)) by A23, A46, A63

      .= (z . (k + 1)) by A57, PARTFUN1:def 6

      .= (f . |.((k + 1) - 1).|) by A24, A27, FINSEQ_1: 4

      .= m by A21, ABSVALUE:def 1;

      then k <= l by A22;

      then ( len z) <= (l + 1) by A23, XREAL_1: 6;

      hence contradiction by A41, A42, XXREAL_0: 2;

    end;

    registration

      cluster non empty strict for RelStr;

      existence

      proof

        set D = the non empty set, f = the Relation of D;

        take RelStr (# D, f #);

        thus the carrier of RelStr (# D, f #) is non empty;

        thus thesis;

      end;

    end

    reserve FT for non empty RelStr;

    reserve x,y,z for Element of FT;

    definition

      let FT be RelStr;

      let x be Element of FT;

      :: FIN_TOPO:def1

      func U_FT x -> Subset of FT equals ( Class (the InternalRel of FT,x));

      coherence ;

    end

    definition

      let x be set, y be Subset of {x};

      :: original: .-->

      redefine

      func x .--> y -> Function of {x}, ( bool {x}) ;

      coherence

      proof

        

         A1: ( dom (x .--> y)) = {x};

        ( rng (x .--> y)) = {y} by FUNCOP_1: 8;

        then

        reconsider R = (x .--> y) as Relation of {x}, ( bool {x}) by A1, RELSET_1: 4;

        R is quasi_total by A1, FUNCT_2:def 1;

        hence thesis;

      end;

    end

    definition

      let x be set;

      :: FIN_TOPO:def2

      func SinglRel x -> Relation of {x} equals { [x, x]};

      coherence

      proof

        x in {x} by TARSKI:def 1;

        hence thesis by RELSET_1: 3;

      end;

    end

    definition

      :: FIN_TOPO:def3

      func FT{0} -> strict RelStr equals RelStr (# { 0 }, ( SinglRel 0 ) #);

      coherence ;

    end

    registration

      cluster FT{0} -> non empty;

      coherence ;

    end

    notation

      let IT be non empty RelStr;

      synonym IT is filled for IT is reflexive;

    end

    definition

      let IT be non empty RelStr;

      :: original: filled

      redefine

      :: FIN_TOPO:def4

      attr IT is filled means

      : Def4: for x be Element of IT holds x in ( U_FT x);

      compatibility

      proof

        thus IT is filled implies for x be Element of IT holds x in ( U_FT x)

        proof

          assume

           A1: IT is filled;

          let x be Element of IT;

          x <= x by A1, ORDERS_2: 1;

          then [x, x] in the InternalRel of IT;

          hence thesis by EQREL_1: 18;

        end;

        assume

         A2: for x be Element of IT holds x in ( U_FT x);

        let x be object;

        assume x in the carrier of IT;

        then

        reconsider x as Element of IT;

        x in ( U_FT x) by A2;

        hence thesis by EQREL_1: 18;

      end;

    end

    theorem :: FIN_TOPO:3

    

     Th3: FT{0} is filled

    proof

      let x be Element of FT{0} ;

      x = 0 & [ 0 , 0 ] in ( SinglRel 0 ) by TARSKI:def 1;

      hence thesis by RELAT_1:def 13;

    end;

    registration

      cluster FT{0} -> filled finite;

      coherence by Th3;

    end

    registration

      cluster finite filled strict for non empty RelStr;

      existence by Th3;

    end

    theorem :: FIN_TOPO:4

    for FT be filled non empty RelStr holds the set of all ( U_FT x) where x be Element of FT is Cover of FT

    proof

      let FT be filled non empty RelStr;

      let a be object;

      assume a in the carrier of FT;

      then

      reconsider b = a as Element of FT;

      b in ( U_FT b) & ( U_FT b) in the set of all ( U_FT x) where x be Element of FT by Def4;

      hence thesis by TARSKI:def 4;

    end;

    reserve A for Subset of FT;

    definition

      let FT;

      let A be Subset of FT;

      :: FIN_TOPO:def5

      func A ^delta -> Subset of FT equals { x : ( U_FT x) meets A & ( U_FT x) meets (A ` ) };

      coherence

      proof

        defpred P[ Element of FT] means ( U_FT $1) meets A & ( U_FT $1) meets (A ` );

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

        hence thesis;

      end;

    end

    theorem :: FIN_TOPO:5

    

     Th5: x in (A ^delta ) iff ( U_FT x) meets A & ( U_FT x) meets (A ` )

    proof

      thus x in (A ^delta ) implies ( U_FT x) meets A & ( U_FT x) meets (A ` )

      proof

        assume x in (A ^delta );

        then ex y st y = x & ( U_FT y) meets A & ( U_FT y) meets (A ` );

        hence thesis;

      end;

      assume ( U_FT x) meets A & ( U_FT x) meets (A ` );

      hence thesis;

    end;

    definition

      let FT;

      let A be Subset of FT;

      :: FIN_TOPO:def6

      func A ^deltai -> Subset of FT equals (A /\ (A ^delta ));

      coherence ;

      :: FIN_TOPO:def7

      func A ^deltao -> Subset of FT equals ((A ` ) /\ (A ^delta ));

      coherence ;

    end

    theorem :: FIN_TOPO:6

    (A ^delta ) = ((A ^deltai ) \/ (A ^deltao ))

    proof

      for x be object holds x in (A ^delta ) iff x in ((A ^deltai ) \/ (A ^deltao ))

      proof

        let x be object;

        thus x in (A ^delta ) implies x in ((A ^deltai ) \/ (A ^deltao ))

        proof

          assume x in (A ^delta );

          then x in (( [#] the carrier of FT) /\ (A ^delta )) by XBOOLE_1: 28;

          then x in ((A \/ (A ` )) /\ (A ^delta )) by SUBSET_1: 10;

          hence thesis by XBOOLE_1: 23;

        end;

        assume x in ((A ^deltai ) \/ (A ^deltao ));

        then x in ((A \/ (A ` )) /\ (A ^delta )) by XBOOLE_1: 23;

        then x in (( [#] the carrier of FT) /\ (A ^delta )) by SUBSET_1: 10;

        hence thesis by XBOOLE_1: 28;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let FT;

      let A be Subset of FT;

      :: FIN_TOPO:def8

      func A ^i -> Subset of FT equals { x : ( U_FT x) c= A };

      coherence

      proof

        defpred P[ Element of FT] means ( U_FT $1) c= A;

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

        hence thesis;

      end;

      :: FIN_TOPO:def9

      func A ^b -> Subset of FT equals { x : ( U_FT x) meets A };

      coherence

      proof

        defpred P[ Element of FT] means ( U_FT $1) meets A;

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

        hence thesis;

      end;

      :: FIN_TOPO:def10

      func A ^s -> Subset of FT equals { x : x in A & (( U_FT x) \ {x}) misses A };

      coherence

      proof

        defpred P[ Element of FT] means $1 in A & (( U_FT $1) \ {$1}) misses A;

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

        hence thesis;

      end;

    end

    definition

      let FT;

      let A be Subset of FT;

      :: FIN_TOPO:def11

      func A ^n -> Subset of FT equals (A \ (A ^s ));

      coherence ;

      :: FIN_TOPO:def12

      func A ^f -> Subset of FT equals { x : ex y st y in A & x in ( U_FT y) };

      coherence

      proof

        defpred P[ Element of FT] means ex y st y in A & $1 in ( U_FT y);

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

        hence thesis;

      end;

    end

    definition

      let IT be non empty RelStr;

      :: FIN_TOPO:def13

      attr IT is symmetric means for x,y be Element of IT holds y in ( U_FT x) implies x in ( U_FT y);

    end

    theorem :: FIN_TOPO:7

    

     Th7: x in (A ^i ) iff ( U_FT x) c= A

    proof

      thus x in (A ^i ) implies ( U_FT x) c= A

      proof

        assume x in (A ^i );

        then ex y st y = x & ( U_FT y) c= A;

        hence thesis;

      end;

      assume ( U_FT x) c= A;

      hence thesis;

    end;

    theorem :: FIN_TOPO:8

    

     Th8: x in (A ^b ) iff ( U_FT x) meets A

    proof

      thus x in (A ^b ) implies ( U_FT x) meets A

      proof

        assume x in (A ^b );

        then ex y st y = x & ( U_FT y) meets A;

        hence thesis;

      end;

      assume ( U_FT x) meets A;

      hence thesis;

    end;

    theorem :: FIN_TOPO:9

    

     Th9: x in (A ^s ) iff x in A & (( U_FT x) \ {x}) misses A

    proof

      thus x in (A ^s ) implies x in A & (( U_FT x) \ {x}) misses A

      proof

        assume x in (A ^s );

        then ex y st y = x & y in A & (( U_FT y) \ {y}) misses A;

        hence thesis;

      end;

      assume x in A & (( U_FT x) \ {x}) misses A;

      hence thesis;

    end;

    theorem :: FIN_TOPO:10

    x in (A ^n ) iff x in A & (( U_FT x) \ {x}) meets A

    proof

      thus x in (A ^n ) implies x in A & (( U_FT x) \ {x}) meets A

      proof

        assume x in (A ^n );

        then x in A & not x in (A ^s ) by XBOOLE_0:def 5;

        hence thesis;

      end;

      assume that

       A1: x in A and

       A2: (( U_FT x) \ {x}) meets A;

       not x in (A ^s ) by A2, Th9;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: FIN_TOPO:11

    

     Th11: x in (A ^f ) iff ex y st y in A & x in ( U_FT y)

    proof

      thus x in (A ^f ) implies ex y st y in A & x in ( U_FT y)

      proof

        assume x in (A ^f );

        then ex y st y = x & ex z st z in A & y in ( U_FT z);

        hence thesis;

      end;

      assume ex z st z in A & x in ( U_FT z);

      hence thesis;

    end;

    theorem :: FIN_TOPO:12

    FT is symmetric iff for A holds (A ^b ) = (A ^f )

    proof

      thus FT is symmetric implies for A holds (A ^b ) = (A ^f )

      proof

        assume

         A1: FT is symmetric;

        let A be Subset of FT;

        thus (A ^b ) c= (A ^f )

        proof

          let x be object;

          assume

           A2: x in (A ^b );

          then

          reconsider y = x as Element of FT;

          ( U_FT y) meets A by A2, Th8;

          then

          consider z be object such that

           A3: z in (( U_FT y) /\ A) by XBOOLE_0: 4;

          reconsider z as Element of FT by A3;

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

          then

           A4: y in ( U_FT z) by A1;

          z in A by A3, XBOOLE_0:def 4;

          hence thesis by A4;

        end;

        let x be object;

        assume

         A5: x in (A ^f );

        then

        reconsider y = x as Element of FT;

        consider z such that

         A6: z in A and

         A7: y in ( U_FT z) by A5, Th11;

        z in ( U_FT y) by A1, A7;

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

        hence thesis;

      end;

      assume

       A8: for A be Subset of FT holds (A ^b ) = (A ^f );

      let x,y be Element of FT;

      assume y in ( U_FT x);

      then ( U_FT x) meets {y} by ZFMISC_1: 48;

      then x in ( {y} ^b );

      then x in ( {y} ^f ) by A8;

      then ex z st z in {y} & x in ( U_FT z) by Th11;

      hence thesis by TARSKI:def 1;

    end;

    reserve F for Subset of FT;

    definition

      let FT;

      let IT be Subset of FT;

      :: FIN_TOPO:def14

      attr IT is open means IT = (IT ^i );

      :: FIN_TOPO:def15

      attr IT is closed means IT = (IT ^b );

      :: FIN_TOPO:def16

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

    end

    definition

      let FT;

      let A be Subset of FT;

      :: FIN_TOPO:def17

      func A ^fb -> Subset of FT equals ( meet { F : A c= F & F is closed });

      coherence

      proof

        set FF = { F : A c= F & F is closed };

        FF c= ( bool the carrier of FT)

        proof

          let x be object;

          assume x in FF;

          then ex F st x = F & A c= F & F is closed;

          hence thesis;

        end;

        then

        reconsider FF as Subset-Family of FT;

        ( meet FF) is Subset of FT;

        hence thesis;

      end;

      :: FIN_TOPO:def18

      func A ^fi -> Subset of FT equals ( union { F : A c= F & F is open });

      coherence

      proof

        set FF = { F : A c= F & F is open };

        FF c= ( bool the carrier of FT)

        proof

          let x be object;

          assume x in FF;

          then ex F st x = F & A c= F & F is open;

          hence thesis;

        end;

        then

        reconsider FF as Subset-Family of FT;

        ( union FF) is Subset of FT;

        hence thesis;

      end;

    end

    theorem :: FIN_TOPO:13

    

     Th13: for FT be filled non empty RelStr, A be Subset of FT holds A c= (A ^b )

    proof

      let FT be filled non empty RelStr;

      let A be Subset of FT;

      let x be object;

      assume

       A1: x in A;

      then

      reconsider y = x as Element of FT;

      y in ( U_FT y) by Def4;

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

      hence thesis;

    end;

    theorem :: FIN_TOPO:14

    

     Th14: for FT be non empty RelStr, A,B be Subset of FT holds A c= B implies (A ^b ) c= (B ^b )

    proof

      let FT be non empty RelStr;

      let A,B be Subset of FT;

      assume

       A1: A c= B;

      let x be object;

      assume

       A2: x in (A ^b );

      then

      reconsider y = x as Element of FT;

      ( U_FT y) meets A by A2, Th8;

      then ex w be object st w in ( U_FT y) & w in A by XBOOLE_0: 3;

      then ( U_FT y) meets B by A1, XBOOLE_0: 3;

      hence thesis;

    end;

    theorem :: FIN_TOPO:15

    for FT be filled finite non empty RelStr, A be Subset of FT holds A is connected iff for x be Element of FT st x in A holds ex S be FinSequence of ( bool the carrier of FT) st ( len S) > 0 & (S /. 1) = {x} & (for i be Element of NAT st i > 0 & i < ( len S) holds (S /. (i + 1)) = (((S /. i) ^b ) /\ A)) & A c= (S /. ( len S))

    proof

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

      thus A is connected implies for x be Element of FT st x in A holds ex S be FinSequence of ( bool the carrier of FT) st ( len S) > 0 & (S /. 1) = {x} & (for i be Element of NAT st i > 0 & i < ( len S) holds (S /. (i + 1)) = (((S /. i) ^b ) /\ A)) & A c= (S /. ( len S))

      proof

        deffunc F( Subset of FT) = (($1 ^b ) /\ A);

        assume

         A1: A is connected;

        let x be Element of FT;

        assume x in A;

        then

         A2: {x} c= A by ZFMISC_1: 31;

        

         A3: for B be Subset of FT st B c= A holds B c= F(B) & F(B) c= A

        proof

          let B be Subset of FT such that

           A4: B c= A;

          B c= (B ^b ) by Th13;

          hence B c= ((B ^b ) /\ A) by A4, XBOOLE_1: 19;

          thus thesis by XBOOLE_1: 17;

        end;

        

         A5: A is finite;

        consider S be FinSequence of ( bool the carrier of FT) such that

         A6: ( len S) > 0 and

         A7: (S /. 1) = {x} and

         A8: for i be Nat st i > 0 & i < ( len S) holds (S /. (i + 1)) = F(/.) and

         A9: F(/.) = (S /. ( len S)) and

         A10: for i,j be Nat st i > 0 & i < j & j <= ( len S) holds (S /. i) c= A & (S /. i) c< (S /. j) from MaxFinSeqEx( A5, A2, A3);

        consider k be Nat such that

         A11: ( len S) = (k + 1) by A6, NAT_1: 6;

        set B = (S /. ( len S));

        set C = (A \ B);

        

         A12: B misses (A \ B) by XBOOLE_1: 79;

        defpred P[ Nat] means $1 < ( len S) implies (S /. ($1 + 1)) <> {} ;

         A13:

        now

          let i be Nat;

          assume

           A14: P[i];

          thus P[(i + 1)]

          proof

            assume

             A15: (i + 1) < ( len S);

            then (i + 1) < ((i + 1) + 1) & ((i + 1) + 1) <= ( len S) by NAT_1: 13;

            then (S /. (i + 1)) c< (S /. ((i + 1) + 1)) by A10;

            then (S /. (i + 1)) c= (S /. ((i + 1) + 1));

            hence thesis by A14, A15, NAT_1: 13;

          end;

        end;

        

         A16: P[ 0 ] by A7;

        

         A17: for i be Nat holds P[i] from NAT_1:sch 2( A16, A13);

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

        k < ( len S) by A11, NAT_1: 13;

        then

         A18: B <> {} by A17, A11;

        take S;

        thus ( len S) > 0 by A6;

        thus (S /. 1) = {x} by A7;

        thus for i be Element of NAT st i > 0 & i < ( len S) holds (S /. (i + 1)) = (((S /. i) ^b ) /\ A) by A8;

        assume not A c= (S /. ( len S));

        then

         A19: C <> {} by XBOOLE_1: 37;

        ((B ^b ) /\ C) = ((B ^b ) /\ (A /\ (A \ B))) by XBOOLE_1: 28, XBOOLE_1: 36

        .= (B /\ (A \ B)) by A9, XBOOLE_1: 16

        .= {} by A12;

        then

         A20: B misses C & (B ^b ) misses C by XBOOLE_1: 79;

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

        .= A by A9, XBOOLE_1: 12, XBOOLE_1: 17;

        hence contradiction by A1, A19, A18, A20;

      end;

      assume

       A21: for x be Element of FT st x in A holds ex S be FinSequence of ( bool the carrier of FT) st ( len S) > 0 & (S /. 1) = {x} & (for i be Element of NAT st i > 0 & i < ( len S) holds (S /. (i + 1)) = (((S /. i) ^b ) /\ A)) & A c= (S /. ( len S));

      given B,C be Subset of FT such that

       A22: A = (B \/ C) and

       A23: B <> {} and

       A24: C <> {} and

       A25: B misses C and

       A26: (B ^b ) misses C;

      set x = the Element of B;

      x in A by A22, A23, XBOOLE_0:def 3;

      then

      consider S be FinSequence of ( bool the carrier of FT) such that

       A27: ( len S) > 0 and

       A28: (S /. 1) = {x} and

       A29: for i be Element of NAT st i > 0 & i < ( len S) holds (S /. (i + 1)) = (((S /. i) ^b ) /\ A) and

       A30: A c= (S /. ( len S)) by A21;

      consider k be Nat such that

       A31: ( len S) = (k + 1) by A27, NAT_1: 6;

      defpred P[ Nat] means $1 < ( len S) implies (S /. ($1 + 1)) c= B;

      ((B ^b ) /\ C) = {} by A26;

      

      then

       A32: ((B ^b ) /\ A) = (((B ^b ) /\ B) \/ {} ) by A22, XBOOLE_1: 23

      .= B by Th13, XBOOLE_1: 28;

       A33:

      now

        let i be Nat;

        assume

         A34: P[i];

        thus P[(i + 1)]

        proof

          assume

           A35: (i + 1) < ( len S);

          then ((S /. (i + 1)) ^b ) c= (B ^b ) by A34, Th14, NAT_1: 13;

          then (((S /. (i + 1)) ^b ) /\ A) c= ((B ^b ) /\ A) by XBOOLE_1: 26;

          hence thesis by A32, A29, A35;

        end;

      end;

      

       A36: P[ 0 ] by A23, A28, ZFMISC_1: 31;

      

       A37: for i be Nat holds P[i] from NAT_1:sch 2( A36, A33);

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

      k < ( len S) by A31, NAT_1: 13;

      then

       A38: (S /. ( len S)) c= B by A37, A31;

      

       A39: B c= A by A22, XBOOLE_1: 7;

      then (S /. ( len S)) c= A by A38;

      then (S /. ( len S)) = A by A30;

      then

       A40: A = B by A39, A38;

      (B /\ C) = {} by A25;

      hence contradiction by A22, A24, A40, XBOOLE_1: 7, XBOOLE_1: 28;

    end;

    theorem :: FIN_TOPO:16

    

     Th16: (((A ` ) ^i ) ` ) = (A ^b )

    proof

      for x be object holds x in (((A ` ) ^i ) ` ) iff x in (A ^b )

      proof

        let x be object;

        thus x in (((A ` ) ^i ) ` ) implies x in (A ^b )

        proof

          assume

           A1: x in (((A ` ) ^i ) ` );

          then

          reconsider y = x as Element of FT;

           not y in ((A ` ) ^i ) by A1, XBOOLE_0:def 5;

          then not ( U_FT y) c= (A ` );

          then

          consider z be object such that

           A2: z in ( U_FT y) and

           A3: not z in (A ` );

          z in A by A2, A3, SUBSET_1: 29;

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

          hence thesis;

        end;

        assume

         A4: x in (A ^b );

        then

        reconsider y = x as Element of FT;

        ( U_FT y) meets A by A4, Th8;

        then ex z be object st z in ( U_FT y) & z in A by XBOOLE_0: 3;

        then not ( U_FT y) c= (A ` ) by XBOOLE_0:def 5;

        then not y in ((A ` ) ^i ) by Th7;

        hence thesis by SUBSET_1: 29;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FIN_TOPO:17

    

     Th17: (((A ` ) ^b ) ` ) = (A ^i )

    proof

      for x be object holds x in (((A ` ) ^b ) ` ) iff x in (A ^i )

      proof

        let x be object;

        thus x in (((A ` ) ^b ) ` ) implies x in (A ^i )

        proof

          assume

           A1: x in (((A ` ) ^b ) ` );

          then

          reconsider y = x as Element of FT;

           not y in ((A ` ) ^b ) by A1, XBOOLE_0:def 5;

          then ( U_FT y) misses (A ` );

          then (( U_FT y) /\ (A ` )) = {} ;

          then (( U_FT y) \ A) = {} by SUBSET_1: 13;

          then ( U_FT y) c= A by XBOOLE_1: 37;

          hence thesis;

        end;

        assume

         A2: x in (A ^i );

        then

        reconsider y = x as Element of FT;

        ( U_FT y) c= A by A2, Th7;

        then (( U_FT y) \ A) = {} by XBOOLE_1: 37;

        then (( U_FT y) /\ (A ` )) = {} by SUBSET_1: 13;

        then ( U_FT y) misses (A ` );

        then not y in ((A ` ) ^b ) by Th8;

        hence thesis by SUBSET_1: 29;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FIN_TOPO:18

    (A ^delta ) = ((A ^b ) /\ ((A ` ) ^b ))

    proof

      for x be object holds x in (A ^delta ) iff x in ((A ^b ) /\ ((A ` ) ^b ))

      proof

        let x be object;

        thus x in (A ^delta ) implies x in ((A ^b ) /\ ((A ` ) ^b ))

        proof

          assume

           A1: x in (A ^delta );

          then

          reconsider y = x as Element of FT;

          ( U_FT y) meets (A ` ) by A1, Th5;

          then

           A2: x in ((A ` ) ^b );

          ( U_FT y) meets A by A1, Th5;

          then x in (A ^b );

          hence thesis by A2, XBOOLE_0:def 4;

        end;

        assume

         A3: x in ((A ^b ) /\ ((A ` ) ^b ));

        then

        reconsider y = x as Element of FT;

        x in ((A ` ) ^b ) by A3, XBOOLE_0:def 4;

        then

         A4: ( U_FT y) meets (A ` ) by Th8;

        x in (A ^b ) by A3, XBOOLE_0:def 4;

        then ( U_FT y) meets A by Th8;

        hence thesis by A4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FIN_TOPO:19

    ((A ` ) ^delta ) = (A ^delta )

    proof

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

      proof

        let x be object;

        thus x in ((A ` ) ^delta ) implies x in (A ^delta )

        proof

          assume

           A1: x in ((A ` ) ^delta );

          then

          reconsider y = x as Element of FT;

          ( U_FT y) meets (A ` ) & ( U_FT y) meets ((A ` ) ` ) by A1, Th5;

          hence thesis;

        end;

        assume

         A2: x in (A ^delta );

        then

        reconsider y = x as Element of FT;

        ( U_FT y) meets ((A ` ) ` ) & ( U_FT y) meets (A ` ) by A2, Th5;

        hence thesis;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FIN_TOPO:20

    x in (A ^s ) implies not x in ((A \ {x}) ^b )

    proof

      assume x in (A ^s );

      then A misses (( U_FT x) \ {x}) by Th9;

      then (A /\ (( U_FT x) \ {x})) = {} ;

      then

       A1: ((A /\ ( U_FT x)) \ {x}) = {} by XBOOLE_1: 49;

      now

        per cases by A1, ZFMISC_1: 58;

          suppose (A /\ ( U_FT x)) = {} ;

          then A misses ( U_FT x);

          hence (A \ {x}) misses ( U_FT x) by XBOOLE_1: 36, XBOOLE_1: 63;

        end;

          suppose (A /\ ( U_FT x)) = {x};

          then ((( U_FT x) /\ A) \ {x}) = {} by XBOOLE_1: 37;

          then (( U_FT x) /\ (A \ {x})) = {} by XBOOLE_1: 49;

          hence (A \ {x}) misses ( U_FT x);

        end;

      end;

      hence thesis by Th8;

    end;

    theorem :: FIN_TOPO:21

    (A ^s ) <> {} & ( card A) <> 1 implies not A is connected

    proof

      assume that

       A1: (A ^s ) <> {} and

       A2: ( card A) <> 1;

      consider z be Element of FT such that

       A3: z in (A ^s ) by A1, SUBSET_1: 4;

      set C = {z};

      set B = (A \ {z});

      ( card {z}) = 1 & A <> {} by A3, Th9, CARD_1: 30;

      then

       A4: B <> {} by A2, ZFMISC_1: 58;

      z in A by A3, Th9;

      then {z} is Subset of A by SUBSET_1: 41;

      then

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

      

       A6: (( U_FT z) \ {z}) misses A by A3, Th9;

      

       A7: (B ^b ) misses C

      proof

        assume (B ^b ) meets C;

        then

        consider x be object such that

         A8: x in (B ^b ) and

         A9: x in C by XBOOLE_0: 3;

        reconsider x as Element of FT by A8;

        

         A10: x = z by A9, TARSKI:def 1;

        ( U_FT x) meets B by A8, Th8;

        then

        consider y be object such that

         A11: y in ( U_FT x) and

         A12: y in B by XBOOLE_0: 3;

         not x in B by A9, XBOOLE_0:def 5;

        then y in (( U_FT x) \ {x}) by A11, A12, ZFMISC_1: 56;

        then (( U_FT z) \ {z}) meets B by A12, A10, XBOOLE_0: 3;

        then

         A13: ex w be object st w in ((( U_FT z) \ {z}) /\ B) by XBOOLE_0: 4;

        ((( U_FT z) \ {z}) /\ B) c= ((( U_FT z) \ {z}) /\ A) by XBOOLE_1: 26, XBOOLE_1: 36;

        hence contradiction by A6, A13;

      end;

      B misses C by XBOOLE_1: 79;

      hence thesis by A5, A4, A7;

    end;

    theorem :: FIN_TOPO:22

    for FT be filled non empty RelStr, A be Subset of FT holds (A ^i ) c= A

    proof

      let FT be filled non empty RelStr;

      let A be Subset of FT;

      let x be object;

      assume

       A1: x in (A ^i );

      then

      reconsider y = x as Element of FT;

      

       A2: y in ( U_FT y) by Def4;

      ( U_FT y) c= A by A1, Th7;

      hence thesis by A2;

    end;

    theorem :: FIN_TOPO:23

    A is open implies (A ` ) is closed

    proof

      assume A is open;

      then

       A1: A = (A ^i );

      (A ^i ) = (((A ` ) ^b ) ` ) by Th17;

      hence thesis by A1;

    end;

    theorem :: FIN_TOPO:24

    A is closed implies (A ` ) is open

    proof

      assume A is closed;

      then

       A1: A = (A ^b );

      (A ^b ) = (((A ` ) ^i ) ` ) by Th16;

      hence thesis by A1;

    end;