fintopo2.miz



    begin

    reserve FT for non empty RelStr;

    reserve A for Subset of FT;

    theorem :: FINTOPO2:1

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

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

      then

      reconsider y = x as Element of FT;

      

       A3: ( U_FT y) c= A by A2, FIN_TOPO: 7;

      for t be Element of FT st t in ( U_FT y) holds t in B by A3, A1;

      then ( U_FT y) c= B;

      hence thesis;

    end;

    theorem :: FINTOPO2:2

    

     Th2: (A ^delta ) = ((A ^b ) /\ ((A ^i ) ` ))

    proof

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

      proof

        let x be object;

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

        proof

          assume

           A1: x in (A ^delta );

          then

          reconsider y = x as Element of FT;

          ( U_FT y) meets (A ` ) by A1, FIN_TOPO: 5;

          then y in ((((A ` ) ^b ) ` ) ` );

          then

           A2: y in ((A ^i ) ` ) by FIN_TOPO: 17;

          ( U_FT y) meets A by A1, FIN_TOPO: 5;

          then y in (A ^b );

          hence thesis by A2, XBOOLE_0:def 4;

        end;

        assume

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

        then

        reconsider y = x as Element of FT;

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

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

        then

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

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

        then ( U_FT y) meets A by FIN_TOPO: 8;

        hence thesis by A4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINTOPO2:3

    (A ^delta ) = ((A ^b ) \ (A ^i ))

    proof

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

      proof

        let x be object;

        thus x in (A ^delta ) implies x in ((A ^b ) \ (A ^i ))

        proof

          assume x in (A ^delta );

          then x in ((A ^b ) /\ ((A ^i ) ` )) by Th2;

          hence thesis by SUBSET_1: 13;

        end;

        assume x in ((A ^b ) \ (A ^i ));

        then x in ((A ^b ) /\ ((A ^i ) ` )) by SUBSET_1: 13;

        hence thesis by Th2;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINTOPO2:4

    (A ` ) is open implies A is closed

    proof

      assume (A ` ) is open;

      then

       A1: (A ` ) = ((A ` ) ^i );

      ((A ` ) ^i ) = ((((A ` ) ` ) ^b ) ` ) by FIN_TOPO: 17

      .= ((A ^b ) ` );

      

      then A = (((A ^b ) ` ) ` ) by A1

      .= (A ^b );

      hence thesis;

    end;

    theorem :: FINTOPO2:5

    (A ` ) is closed implies A is open

    proof

      assume (A ` ) is closed;

      then

       A1: (A ` ) = ((A ` ) ^b );

      ((A ` ) ^b ) = ((((A ` ) ` ) ^i ) ` ) by FIN_TOPO: 16

      .= ((A ^i ) ` );

      

      then A = (((A ^i ) ` ) ` ) by A1

      .= (A ^i );

      hence thesis;

    end;

    definition

      let FT be non empty RelStr;

      let x be Element of FT;

      let y be Element of FT;

      let A be Subset of FT;

      :: FINTOPO2:def1

      func P_1 (x,y,A) -> Element of BOOLEAN equals

      : Def1: TRUE if y in ( U_FT x) & y in A

      otherwise FALSE ;

      correctness ;

    end

    definition

      let FT be non empty RelStr;

      let x be Element of FT;

      let y be Element of FT;

      let A be Subset of FT;

      :: FINTOPO2:def2

      func P_2 (x,y,A) -> Element of BOOLEAN equals

      : Def2: TRUE if y in ( U_FT x) & y in (A ` )

      otherwise FALSE ;

      correctness ;

    end

    theorem :: FINTOPO2:6

    for x,y be Element of FT, A be Subset of FT holds ( P_1 (x,y,A)) = TRUE iff y in ( U_FT x) & y in A by Def1;

    theorem :: FINTOPO2:7

    for x,y be Element of FT, A be Subset of FT holds ( P_2 (x,y,A)) = TRUE iff y in ( U_FT x) & y in (A ` ) by Def2;

    theorem :: FINTOPO2:8

    

     Th8: for x be Element of FT, A be Subset of FT holds x in (A ^delta ) iff ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE

    proof

      let x be Element of FT;

      let A be Subset of FT;

      

       A1: x in (A ^delta ) implies ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE

      proof

        reconsider z = x as Element of FT;

        assume

         A2: x in (A ^delta );

        then ( U_FT z) meets A by FIN_TOPO: 5;

        then

        consider w1 be object such that

         A3: w1 in ( U_FT z) and

         A4: w1 in A by XBOOLE_0: 3;

        reconsider w1 as Element of FT by A3;

        take w1;

        ( U_FT z) meets (A ` ) by A2, FIN_TOPO: 5;

        then

        consider w2 be object such that

         A5: w2 in ( U_FT z) & w2 in (A ` ) by XBOOLE_0: 3;

        take w2;

        thus thesis by A3, A4, A5, Def1, Def2;

      end;

      (ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE ) implies x in (A ^delta )

      proof

        given y1,y2 be Element of FT such that

         A6: ( P_1 (x,y1,A)) = TRUE and

         A7: ( P_2 (x,y2,A)) = TRUE ;

        y1 in ( U_FT x) & y1 in A by A6, Def1;

        then (( U_FT x) /\ A) <> {} by XBOOLE_0:def 4;

        then

         A8: ( U_FT x) meets A;

        y2 in ( U_FT x) & y2 in (A ` ) by A7, Def2;

        then ( U_FT x) meets (A ` ) by XBOOLE_0: 3;

        hence thesis by A8;

      end;

      hence thesis by A1;

    end;

    definition

      let FT be non empty RelStr;

      let x be Element of FT;

      let y be Element of FT;

      :: FINTOPO2:def3

      func P_0 (x,y) -> Element of BOOLEAN equals

      : Def3: TRUE if y in ( U_FT x)

      otherwise FALSE ;

      correctness ;

    end

    theorem :: FINTOPO2:9

    for x,y be Element of FT holds ( P_0 (x,y)) = TRUE iff y in ( U_FT x) by Def3;

    theorem :: FINTOPO2:10

    for x be Element of FT, A be Subset of FT holds x in (A ^i ) iff for y be Element of FT holds (( P_0 (x,y)) = TRUE implies ( P_1 (x,y,A)) = TRUE )

    proof

      let x be Element of FT;

      let A be Subset of FT;

      

       A1: (for y be Element of FT holds (( P_0 (x,y)) = TRUE implies ( P_1 (x,y,A)) = TRUE )) implies x in (A ^i )

      proof

        assume

         A2: for y be Element of FT holds (( P_0 (x,y)) = TRUE implies ( P_1 (x,y,A)) = TRUE );

        for y be Element of FT holds y in ( U_FT x) implies y in ( U_FT x) & y in A

        proof

          let y be Element of FT;

          assume y in ( U_FT x);

          then ( P_0 (x,y)) = TRUE by Def3;

          then ( P_1 (x,y,A)) = TRUE by A2;

          hence thesis by Def1;

        end;

        then for y be Element of FT holds y in ( U_FT x) implies y in A;

        then ( U_FT x) c= A;

        hence thesis;

      end;

      x in (A ^i ) implies for y be Element of FT holds (( P_0 (x,y)) = TRUE implies ( P_1 (x,y,A)) = TRUE )

      proof

        assume x in (A ^i );

        then

         A3: ( U_FT x) c= A by FIN_TOPO: 7;

        let y be Element of FT;

        assume ( P_0 (x,y)) = TRUE ;

        then y in ( U_FT x) by Def3;

        hence thesis by A3, Def1;

      end;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:11

    for x be Element of FT, A be Subset of FT holds x in (A ^b ) iff ex y1 be Element of FT st ( P_1 (x,y1,A)) = TRUE

    proof

      let x be Element of FT;

      let A be Subset of FT;

      

       A1: x in (A ^b ) implies ex y1 be Element of FT st ( P_1 (x,y1,A)) = TRUE

      proof

        reconsider z = x as Element of FT;

        assume x in (A ^b );

        then ( U_FT z) meets A by FIN_TOPO: 8;

        then

        consider w be object such that

         A2: w in ( U_FT z) and

         A3: w in A by XBOOLE_0: 3;

        reconsider w as Element of FT by A2;

        take w;

        thus thesis by A2, A3, Def1;

      end;

      (ex y1 be Element of FT st ( P_1 (x,y1,A)) = TRUE ) implies x in (A ^b )

      proof

        given y be Element of FT such that

         A4: ( P_1 (x,y,A)) = TRUE ;

        y in ( U_FT x) & y in A by A4, Def1;

        then y in (( U_FT x) /\ A) by XBOOLE_0:def 4;

        then ( U_FT x) meets A;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    definition

      let FT be non empty RelStr;

      let x be Element of FT;

      let A be Subset of FT;

      :: FINTOPO2:def4

      func P_A (x,A) -> Element of BOOLEAN equals

      : Def4: TRUE if x in A

      otherwise FALSE ;

      correctness ;

    end

    theorem :: FINTOPO2:12

    for x be Element of FT, A be Subset of FT holds ( P_A (x,A)) = TRUE iff x in A by Def4;

    theorem :: FINTOPO2:13

    for x be Element of FT, A be Subset of FT holds x in (A ^deltai ) iff (ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE ) & ( P_A (x,A)) = TRUE

    proof

      let x be Element of FT;

      let A be Subset of FT;

      

       A1: (ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE ) & ( P_A (x,A)) = TRUE implies x in (A ^deltai )

      proof

        assume (ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE ) & ( P_A (x,A)) = TRUE ;

        then x in (A ^delta ) & x in A by Def4, Th8;

        hence thesis by XBOOLE_0:def 4;

      end;

      x in (A ^deltai ) implies (ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE ) & ( P_A (x,A)) = TRUE

      proof

        assume x in (A ^deltai );

        then x in A & x in (A ^delta ) by XBOOLE_0:def 4;

        hence thesis by Def4, Th8;

      end;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:14

    for x be Element of FT, A be Subset of FT holds x in (A ^deltao ) iff (ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE ) & ( P_A (x,A)) = FALSE

    proof

      let x be Element of FT;

      let A be Subset of FT;

      

       A1: (ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE ) & ( P_A (x,A)) = FALSE implies x in (A ^deltao )

      proof

        assume that

         A2: ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE and

         A3: ( P_A (x,A)) = FALSE ;

         not x in A by A3, Def4;

        then

         A4: x in (A ` ) by XBOOLE_0:def 5;

        x in (A ^delta ) by A2, Th8;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      x in (A ^deltao ) implies (ex y1,y2 be Element of FT st ( P_1 (x,y1,A)) = TRUE & ( P_2 (x,y2,A)) = TRUE ) & ( P_A (x,A)) = FALSE

      proof

        assume

         A5: x in (A ^deltao );

        then x in (A ` ) by XBOOLE_0:def 4;

        then

         A6: not x in A by XBOOLE_0:def 5;

        x in (A ^delta ) by A5, XBOOLE_0:def 4;

        hence thesis by A6, Def4, Th8;

      end;

      hence thesis by A1;

    end;

    definition

      let FT be non empty RelStr;

      let x be Element of FT;

      let y be Element of FT;

      :: FINTOPO2:def5

      func P_e (x,y) -> Element of BOOLEAN equals

      : Def5: TRUE if x = y

      otherwise FALSE ;

      correctness ;

    end

    theorem :: FINTOPO2:15

    for x,y be Element of FT holds ( P_e (x,y)) = TRUE iff x = y by Def5;

    theorem :: FINTOPO2:16

    for x be Element of FT, A be Subset of FT holds x in (A ^s ) iff ( P_A (x,A)) = TRUE & not (ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE )

    proof

      let x be Element of FT;

      let A be Subset of FT;

      

       A1: x in (A ^s ) implies ( P_A (x,A)) = TRUE & not (ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE )

      proof

        assume

         A2: x in (A ^s );

        then (( U_FT x) \ {x}) misses A by FIN_TOPO: 9;

        then

         A3: ((( U_FT x) \ {x}) /\ A) = {} ;

        

         A4: not (ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE )

        proof

          given y be Element of FT such that

           A5: ( P_1 (x,y,A)) = TRUE and

           A6: ( P_e (x,y)) = FALSE ;

           not x = y by A6, Def5;

          then

           A7: not y in {x} by TARSKI:def 1;

          y in ( U_FT x) by A5, Def1;

          then

           A8: y in (( U_FT x) \ {x}) by A7, XBOOLE_0:def 5;

          y in A by A5, Def1;

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

        end;

        x in A by A2, FIN_TOPO: 9;

        hence thesis by A4, Def4;

      end;

      ( P_A (x,A)) = TRUE & not (ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE ) implies x in (A ^s )

      proof

        assume that

         A9: ( P_A (x,A)) = TRUE and

         A10: not (ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE );

        for y be Element of FT holds not y in ((( U_FT x) \ {x}) /\ A)

        proof

          let y be Element of FT;

           not (( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE ) by A10;

          then not (y in ( U_FT x) & ( not x = y) & y in A) by Def1, Def5;

          then not (y in ( U_FT x) & ( not y in {x}) & y in A) by TARSKI:def 1;

          then not (y in (( U_FT x) \ {x}) & y in A) by XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 4;

        end;

        then ((( U_FT x) \ {x}) /\ A) = {} by SUBSET_1: 4;

        then

         A11: (( U_FT x) \ {x}) misses A;

        x in A by A9, Def4;

        hence thesis by A11;

      end;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:17

    for x be Element of FT, A be Subset of FT holds x in (A ^n ) iff ( P_A (x,A)) = TRUE & ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE

    proof

      let x be Element of FT;

      let A be Subset of FT;

      

       A1: x in (A ^n ) implies ( P_A (x,A)) = TRUE & ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE

      proof

        assume

         A2: x in (A ^n );

        then (( U_FT x) \ {x}) meets A by FIN_TOPO: 10;

        then ((( U_FT x) \ {x}) /\ A) <> {} ;

        then

        consider y be Element of FT such that

         A3: y in ((( U_FT x) \ {x}) /\ A) by SUBSET_1: 4;

        

         A4: y in (( U_FT x) \ {x}) by A3, XBOOLE_0:def 4;

        then

         A5: y in ( U_FT x) by XBOOLE_0:def 5;

         not y in {x} by A4, XBOOLE_0:def 5;

        then not x = y by TARSKI:def 1;

        then

         A6: ( P_e (x,y)) = FALSE by Def5;

        y in A by A3, XBOOLE_0:def 4;

        then

         A7: ( P_1 (x,y,A)) = TRUE by A5, Def1;

        x in A by A2, FIN_TOPO: 10;

        hence thesis by A6, A7, Def4;

      end;

      (( P_A (x,A)) = TRUE & ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE ) implies x in (A ^n )

      proof

        assume that

         A8: ( P_A (x,A)) = TRUE and

         A9: ex y be Element of FT st ( P_1 (x,y,A)) = TRUE & ( P_e (x,y)) = FALSE ;

        consider y be Element of FT such that

         A10: ( P_1 (x,y,A)) = TRUE and

         A11: ( P_e (x,y)) = FALSE by A9;

        x <> y by A11, Def5;

        then

         A12: not y in {x} by TARSKI:def 1;

        y in ( U_FT x) by A10, Def1;

        then

         A13: y in (( U_FT x) \ {x}) by A12, XBOOLE_0:def 5;

        y in A by A10, Def1;

        then

         A14: (( U_FT x) \ {x}) meets A by A13, XBOOLE_0: 3;

        x in A by A8, Def4;

        hence thesis by A14, FIN_TOPO: 10;

      end;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:18

    for x be Element of FT, A be Subset of FT holds x in (A ^f ) iff ex y be Element of FT st ( P_A (y,A)) = TRUE & ( P_0 (y,x)) = TRUE

    proof

      let x be Element of FT;

      let A be Subset of FT;

      

       A1: (ex y be Element of FT st ( P_A (y,A)) = TRUE & ( P_0 (y,x)) = TRUE ) implies x in (A ^f )

      proof

        assume ex y be Element of FT st ( P_A (y,A)) = TRUE & ( P_0 (y,x)) = TRUE ;

        then

        consider y be Element of FT such that

         A2: ( P_A (y,A)) = TRUE & ( P_0 (y,x)) = TRUE ;

        y in A & x in ( U_FT y) by A2, Def3, Def4;

        hence thesis;

      end;

      x in (A ^f ) implies ex y be Element of FT st ( P_A (y,A)) = TRUE & ( P_0 (y,x)) = TRUE

      proof

        assume x in (A ^f );

        then

        consider y be Element of FT such that

         A3: y in A & x in ( U_FT y) by FIN_TOPO: 11;

        ( P_A (y,A)) = TRUE & ( P_0 (y,x)) = TRUE by A3, Def3, Def4;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    begin

    definition

      struct ( 1-sorted) FMT_Space_Str (# the carrier -> set,

the BNbd -> Function of the carrier, ( bool ( bool the carrier)) #)

       attr strict strict;

    end

    registration

      cluster non empty strict for FMT_Space_Str;

      existence

      proof

        set D = the non empty set, f = the Function of D, ( bool ( bool D));

        take FMT_Space_Str (# D, f #);

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

        thus thesis;

      end;

    end

    reserve T for non empty TopStruct;

    reserve FMT for non empty FMT_Space_Str;

    reserve x,y for Element of FMT;

    definition

      let FMT;

      let x be Element of FMT;

      :: FINTOPO2:def6

      func U_FMT x -> Subset-Family of FMT equals (the BNbd of FMT . x);

      correctness ;

    end

    definition

      let T;

      :: FINTOPO2:def7

      func NeighSp T -> non empty strict FMT_Space_Str means the carrier of it = the carrier of T & for x be Point of it holds ( U_FMT x) = { V where V be Subset of T : V in the topology of T & x in V };

      existence

      proof

        ex IT be non empty strict FMT_Space_Str st the carrier of IT = the carrier of T & for x be Point of IT holds ( U_FMT x) = { V where V be Subset of T : V in the topology of T & x in V }

        proof

          deffunc F( set) = { V where V be Subset of T : V in the topology of T & $1 in V };

          

           A1: for x be Element of T holds F(x) in ( bool ( bool the carrier of T))

          proof

            let x be Element of T;

            now

              let Y be object;

              assume Y in { V where V be Subset of T : V in the topology of T & x in V };

              then ex V be Subset of T st V = Y & V in the topology of T & x in V;

              hence Y in ( bool the carrier of T);

            end;

            then { V where V be Subset of T : V in the topology of T & x in V } c= ( bool the carrier of T);

            hence thesis;

          end;

          consider f be Function of the carrier of T, ( bool ( bool the carrier of T)) such that

           A2: for x be Element of T holds (f . x) = F(x) from FUNCT_2:sch 8( A1);

          reconsider IT = FMT_Space_Str (# the carrier of T, f #) as non empty strict FMT_Space_Str;

          take IT;

          thus thesis by A2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let it1,it2 be non empty strict FMT_Space_Str such that

         A3: the carrier of it1 = the carrier of T and

         A4: for x be Point of it1 holds ( U_FMT x) = { V where V be Subset of T : V in the topology of T & x in V } and

         A5: the carrier of it2 = the carrier of T and

         A6: for x be Point of it2 holds ( U_FMT x) = { V where V be Subset of T : V in the topology of T & x in V };

        

         A7: for x be Element of it2 holds (the BNbd of it2 . x) = { V where V be Subset of T : V in the topology of T & x in V }

        proof

          let x be Element of it2;

          (the BNbd of it2 . x) = ( U_FMT x);

          hence thesis by A6;

        end;

        

         A8: for x be Element of it1 holds (the BNbd of it1 . x) = { V where V be Subset of T : V in the topology of T & x in V }

        proof

          let x be Element of it1;

          (the BNbd of it1 . x) = ( U_FMT x);

          hence thesis by A4;

        end;

        now

          let x be Point of it1;

          

          thus (the BNbd of it1 . x) = { V where V be Subset of T : V in the topology of T & x in V } by A8

          .= (the BNbd of it2 . x) by A3, A5, A7;

        end;

        hence thesis by A3, A5, FUNCT_2: 63;

      end;

    end

    reserve A,B,W,V for Subset of FMT;

    definition

      let IT be non empty FMT_Space_Str;

      :: FINTOPO2:def8

      attr IT is Fo_filled means for x be Element of IT holds for D be Subset of IT st D in ( U_FMT x) holds x in D;

    end

    definition

      let FMT;

      let A;

      :: FINTOPO2:def9

      func A ^Fodelta -> Subset of FMT equals { x : for W st W in ( U_FMT x) holds W meets A & W meets (A ` ) };

      coherence

      proof

        defpred P[ Element of FMT] means for W st W in ( U_FMT $1) holds W meets A & W meets (A ` );

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

        hence thesis;

      end;

    end

    theorem :: FINTOPO2:19

    

     Th19: x in (A ^Fodelta ) iff for W st W in ( U_FMT x) holds W meets A & W meets (A ` )

    proof

      thus x in (A ^Fodelta ) implies for W st W in ( U_FMT x) holds W meets A & W meets (A ` )

      proof

        assume x in (A ^Fodelta );

        then ex y st y = x & for W st W in ( U_FMT y) holds W meets A & W meets (A ` );

        hence thesis;

      end;

      assume for W st W in ( U_FMT x) holds W meets A & W meets (A ` );

      hence thesis;

    end;

    definition

      let FMT, A;

      :: FINTOPO2:def10

      func A ^Fob -> Subset of FMT equals { x : for W st W in ( U_FMT x) holds W meets A };

      coherence

      proof

        defpred P[ Element of FMT] means for W st W in ( U_FMT $1) holds W meets A;

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

        hence thesis;

      end;

    end

    theorem :: FINTOPO2:20

    

     Th20: x in (A ^Fob ) iff for W st W in ( U_FMT x) holds W meets A

    proof

      thus x in (A ^Fob ) implies for W st W in ( U_FMT x) holds W meets A

      proof

        assume x in (A ^Fob );

        then ex y st y = x & for W st W in ( U_FMT y) holds W meets A;

        hence thesis;

      end;

      assume for W st W in ( U_FMT x) holds W meets A;

      hence thesis;

    end;

    definition

      let FMT, A;

      :: FINTOPO2:def11

      func A ^Foi -> Subset of FMT equals { x : ex V st V in ( U_FMT x) & V c= A };

      coherence

      proof

        defpred P[ Element of FMT] means ex V st V in ( U_FMT $1) & V c= A;

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

        hence thesis;

      end;

    end

    theorem :: FINTOPO2:21

    

     Th21: x in (A ^Foi ) iff ex V st V in ( U_FMT x) & V c= A

    proof

      thus x in (A ^Foi ) implies ex V st V in ( U_FMT x) & V c= A

      proof

        assume x in (A ^Foi );

        then ex y st y = x & ex V st V in ( U_FMT y) & V c= A;

        hence thesis;

      end;

      assume ex V st V in ( U_FMT x) & V c= A;

      hence thesis;

    end;

    definition

      let FMT, A;

      :: FINTOPO2:def12

      func A ^Fos -> Subset of FMT equals { x : x in A & (ex V st V in ( U_FMT x) & (V \ {x}) misses A) };

      coherence

      proof

        defpred P[ Element of FMT] means $1 in A & (ex V st V in ( U_FMT $1) & (V \ {$1}) misses A);

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

        hence thesis;

      end;

    end

    theorem :: FINTOPO2:22

    

     Th22: x in (A ^Fos ) iff x in A & ex V st V in ( U_FMT x) & (V \ {x}) misses A

    proof

      thus x in (A ^Fos ) implies x in A & ex V st V in ( U_FMT x) & (V \ {x}) misses A

      proof

        assume x in (A ^Fos );

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

        hence thesis;

      end;

      assume x in A & ex V st V in ( U_FMT x) & (V \ {x}) misses A;

      hence thesis;

    end;

    definition

      let FMT, A;

      :: FINTOPO2:def13

      func A ^Fon -> Subset of FMT equals (A \ (A ^Fos ));

      coherence ;

    end

    theorem :: FINTOPO2:23

    x in (A ^Fon ) iff x in A & for V st V in ( U_FMT x) holds (V \ {x}) meets A

    proof

      thus x in (A ^Fon ) implies x in A & for V st V in ( U_FMT x) holds (V \ {x}) meets A

      proof

        assume x in (A ^Fon );

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

        hence thesis;

      end;

      assume that

       A1: x in A and

       A2: for V st V in ( U_FMT x) holds (V \ {x}) meets A;

       not x in (A ^Fos ) by A2, Th22;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: FINTOPO2:24

    

     Th24: for FMT be non empty FMT_Space_Str, A,B be Subset of FMT holds A c= B implies (A ^Fob ) c= (B ^Fob )

    proof

      let FMT be non empty FMT_Space_Str;

      let A,B be Subset of FMT;

      assume

       A1: A c= B;

      let x be object;

      assume

       A2: x in (A ^Fob );

      then

      reconsider y = x as Element of FMT;

      for W be Subset of FMT st W in ( U_FMT y) holds W meets B

      proof

        let W be Subset of FMT;

        assume W in ( U_FMT y);

        then W meets A by A2, Th20;

        then ex z be object st z in W & z in A by XBOOLE_0: 3;

        hence (W /\ B) <> {} by A1, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO2:25

    

     Th25: for FMT be non empty FMT_Space_Str, A,B be Subset of FMT holds A c= B implies (A ^Foi ) c= (B ^Foi )

    proof

      let FMT be non empty FMT_Space_Str;

      let A,B be Subset of FMT;

      assume

       A1: A c= B;

      let x be object;

      assume

       A2: x in (A ^Foi );

      then

      reconsider y = x as Element of FMT;

      consider V9 be Subset of FMT such that

       A3: V9 in ( U_FMT y) and

       A4: V9 c= A by A2, Th21;

      V9 c= B by A1, A4;

      hence thesis by A3;

    end;

    theorem :: FINTOPO2:26

    

     Th26: ((A ^Fob ) \/ (B ^Fob )) c= ((A \/ B) ^Fob )

    proof

      let x be object;

      assume x in ((A ^Fob ) \/ (B ^Fob ));

      then

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

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

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:27

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

    proof

      let x be object;

      assume

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

      ((A /\ B) ^Fob ) c= (A ^Fob ) & ((B /\ A) ^Fob ) c= (B ^Fob ) by Th24, XBOOLE_1: 17;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: FINTOPO2:28

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

    proof

      let x be object;

      assume x in ((A ^Foi ) \/ (B ^Foi ));

      then

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

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

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:29

    

     Th29: ((A /\ B) ^Foi ) c= ((A ^Foi ) /\ (B ^Foi ))

    proof

      let x be object;

      assume

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

      ((A /\ B) ^Foi ) c= (A ^Foi ) & ((B /\ A) ^Foi ) c= (B ^Foi ) by Th25, XBOOLE_1: 17;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: FINTOPO2:30

    for FMT be non empty FMT_Space_Str holds (for x be Element of FMT, V1,V2 be Subset of FMT st ((V1 in ( U_FMT x)) & (V2 in ( U_FMT x))) holds ex W be Subset of FMT st ((W in ( U_FMT x)) & (W c= (V1 /\ V2)))) iff for A,B be Subset of FMT holds ((A \/ B) ^Fob ) = ((A ^Fob ) \/ (B ^Fob ))

    proof

      let FMT be non empty FMT_Space_Str;

      

       A1: (for x be Element of FMT, V1,V2 be Subset of FMT st ((V1 in ( U_FMT x)) & (V2 in ( U_FMT x))) holds ex W be Subset of FMT st ((W in ( U_FMT x)) & (W c= (V1 /\ V2)))) implies for A,B be Subset of FMT holds ((A \/ B) ^Fob ) = ((A ^Fob ) \/ (B ^Fob ))

      proof

        assume

         A2: for x be Element of FMT, V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds ex W be Subset of FMT st W in ( U_FMT x) & W c= (V1 /\ V2);

        let A,B be Subset of FMT;

        for x be Element of FMT holds x in ((A \/ B) ^Fob ) iff x in ((A ^Fob ) \/ (B ^Fob ))

        proof

          let x be Element of FMT;

          

           A3: x in ((A \/ B) ^Fob ) implies x in ((A ^Fob ) \/ (B ^Fob ))

          proof

            assume

             A4: x in ((A \/ B) ^Fob );

            

             A5: for W1 be Subset of FMT st W1 in ( U_FMT x) holds W1 meets A or W1 meets B

            proof

              let W1 be Subset of FMT;

              assume W1 in ( U_FMT x);

              then W1 meets (A \/ B) by A4, Th20;

              then (W1 /\ (A \/ B)) <> {} ;

              then ((W1 /\ A) \/ (W1 /\ B)) <> {} by XBOOLE_1: 23;

              then (W1 /\ A) <> {} or (W1 /\ B) <> {} ;

              hence thesis;

            end;

            for V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds (V1 meets A or V2 meets B)

            proof

              let V1,V2 be Subset of FMT;

              assume V1 in ( U_FMT x) & V2 in ( U_FMT x);

              then

              consider W be Subset of FMT such that

               A6: W in ( U_FMT x) and

               A7: W c= (V1 /\ V2) by A2;

              (V1 /\ V2) c= V1 by XBOOLE_1: 17;

              then W c= V1 by A7;

              then

               A8: (W /\ A) c= (V1 /\ A) by XBOOLE_1: 26;

              (V1 /\ V2) c= V2 by XBOOLE_1: 17;

              then W c= V2 by A7;

              then

               A9: (W /\ B) c= (V2 /\ B) by XBOOLE_1: 26;

              W meets A or W meets B by A5, A6;

              then (W /\ A) <> {} or (W /\ B) <> {} ;

              then ex z1,z2 be Element of FMT st (z1 in (W /\ A) or z2 in (W /\ B)) by SUBSET_1: 4;

              hence thesis by A8, A9;

            end;

            then (for V1 be Subset of FMT st V1 in ( U_FMT x) holds V1 meets A) or for V2 be Subset of FMT st V2 in ( U_FMT x) holds V2 meets B;

            then x in (A ^Fob ) or x in (B ^Fob );

            hence thesis by XBOOLE_0:def 3;

          end;

          x in ((A ^Fob ) \/ (B ^Fob )) implies x in ((A \/ B) ^Fob )

          proof

            assume

             A10: x in ((A ^Fob ) \/ (B ^Fob ));

            ((A ^Fob ) \/ (B ^Fob )) c= ((A \/ B) ^Fob ) by Th26;

            hence thesis by A10;

          end;

          hence thesis by A3;

        end;

        hence thesis by SUBSET_1: 3;

      end;

      (ex x be Element of FMT, V1,V2 be Subset of FMT st (V1 in ( U_FMT x)) & (V2 in ( U_FMT x)) & (for W be Subset of FMT st W in ( U_FMT x) holds ( not (W c= (V1 /\ V2))))) implies ex A,B be Subset of FMT st ((A \/ B) ^Fob ) <> ((A ^Fob ) \/ (B ^Fob ))

      proof

        given x0 be Element of FMT, V1,V2 be Subset of FMT such that

         A11: V1 in ( U_FMT x0) and

         A12: V2 in ( U_FMT x0) and

         A13: for W be Subset of FMT st W in ( U_FMT x0) holds not W c= (V1 /\ V2);

        

         A14: not x0 in ((V2 ` ) ^Fob )

        proof

          

           A15: V2 misses (V2 ` ) by XBOOLE_1: 79;

          assume x0 in ((V2 ` ) ^Fob );

          hence contradiction by A12, A15, Th20;

        end;

        take (V1 ` ), (V2 ` );

        for W be Subset of FMT st W in ( U_FMT x0) holds W meets ((V1 ` ) \/ (V2 ` ))

        proof

          let W be Subset of FMT;

          assume W in ( U_FMT x0);

          then

           A16: not W c= (V1 /\ V2) by A13;

          (W /\ ((V1 /\ V2) ` )) <> {}

          proof

            assume (W /\ ((V1 /\ V2) ` )) = {} ;

            then (W \ (V1 /\ V2)) = {} by SUBSET_1: 13;

            hence contradiction by A16, XBOOLE_1: 37;

          end;

          hence (W /\ ((V1 ` ) \/ (V2 ` ))) <> {} by XBOOLE_1: 54;

        end;

        then

         A17: x0 in (((V1 ` ) \/ (V2 ` )) ^Fob );

         not x0 in ((V1 ` ) ^Fob )

        proof

          

           A18: V1 misses (V1 ` ) by XBOOLE_1: 79;

          assume x0 in ((V1 ` ) ^Fob );

          hence contradiction by A11, A18, Th20;

        end;

        hence thesis by A17, A14, XBOOLE_0:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:31

    for FMT be non empty FMT_Space_Str holds (for x be Element of FMT, V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds ex W be Subset of FMT st (W in ( U_FMT x) & W c= (V1 /\ V2))) iff for A,B be Subset of FMT holds ((A ^Foi ) /\ (B ^Foi )) = ((A /\ B) ^Foi )

    proof

      let FMT be non empty FMT_Space_Str;

      thus (for x be Element of FMT, V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds ex W be Subset of FMT st (W in ( U_FMT x) & W c= (V1 /\ V2))) implies for A,B be Subset of FMT holds ((A ^Foi ) /\ (B ^Foi )) = ((A /\ B) ^Foi )

      proof

        assume

         A1: for x be Element of FMT, V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds ex W be Subset of FMT st W in ( U_FMT x) & W c= (V1 /\ V2);

        let A,B be Subset of FMT;

        for x be Element of FMT holds x in ((A ^Foi ) /\ (B ^Foi )) iff x in ((A /\ B) ^Foi )

        proof

          let x be Element of FMT;

          

           A2: x in ((A ^Foi ) /\ (B ^Foi )) implies x in ((A /\ B) ^Foi )

          proof

            assume

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

            then x in (B ^Foi ) by XBOOLE_0:def 4;

            then

             A4: ex W2 be Subset of FMT st W2 in ( U_FMT x) & W2 c= B by Th21;

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

            then ex W1 be Subset of FMT st W1 in ( U_FMT x) & W1 c= A by Th21;

            then

            consider W1,W2 be Subset of FMT such that

             A5: W1 in ( U_FMT x) & W2 in ( U_FMT x) and

             A6: W1 c= A and

             A7: W2 c= B by A4;

            consider W be Subset of FMT such that

             A8: W in ( U_FMT x) and

             A9: W c= (W1 /\ W2) by A1, A5;

            (W1 /\ W2) c= W2 by XBOOLE_1: 17;

            then W c= W2 by A9;

            then

             A10: W c= B by A7;

            (W1 /\ W2) c= W1 by XBOOLE_1: 17;

            then W c= W1 by A9;

            then W c= A by A6;

            then W c= (A /\ B) by A10, XBOOLE_1: 19;

            hence thesis by A8;

          end;

          x in ((A /\ B) ^Foi ) implies x in ((A ^Foi ) /\ (B ^Foi ))

          proof

            assume

             A11: x in ((A /\ B) ^Foi );

            ((A /\ B) ^Foi ) c= ((A ^Foi ) /\ (B ^Foi )) by Th29;

            hence thesis by A11;

          end;

          hence thesis by A2;

        end;

        hence ((A ^Foi ) /\ (B ^Foi )) = ((A /\ B) ^Foi ) by SUBSET_1: 3;

      end;

      (ex x be Element of FMT, V1,V2 be Subset of FMT st (V1 in ( U_FMT x) & V2 in ( U_FMT x)) & (for W be Subset of FMT st W in ( U_FMT x) holds ( not (W c= (V1 /\ V2))))) implies ex A,B be Subset of FMT st ((A ^Foi ) /\ (B ^Foi )) <> ((A /\ B) ^Foi )

      proof

        given x0 be Element of FMT, V1,V2 be Subset of FMT such that

         A12: V1 in ( U_FMT x0) & V2 in ( U_FMT x0) and

         A13: for W be Subset of FMT st W in ( U_FMT x0) holds not W c= (V1 /\ V2);

        take V1, V2;

        x0 in (V1 ^Foi ) & x0 in (V2 ^Foi ) by A12;

        then x0 in ((V1 ^Foi ) /\ (V2 ^Foi )) by XBOOLE_0:def 4;

        hence thesis by A13, Th21;

      end;

      hence (for A,B be Subset of FMT holds ((A ^Foi ) /\ (B ^Foi )) = ((A /\ B) ^Foi )) implies for x be Element of FMT, V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds ex W be Subset of FMT st W in ( U_FMT x) & W c= (V1 /\ V2);

    end;

    theorem :: FINTOPO2:32

    for FMT be non empty FMT_Space_Str, A,B be Subset of FMT holds (for x be Element of FMT, V1,V2 be Subset of FMT st ((V1 in ( U_FMT x)) & V2 in ( U_FMT x)) holds ex W be Subset of FMT st ((W in ( U_FMT x)) & (W c= (V1 /\ V2)))) implies ((A \/ B) ^Fodelta ) c= ((A ^Fodelta ) \/ (B ^Fodelta ))

    proof

      let FMT be non empty FMT_Space_Str;

      let A,B be Subset of FMT;

      assume

       A1: for x be Element of FMT, V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds ex W be Subset of FMT st W in ( U_FMT x) & W c= (V1 /\ V2);

      for x be Element of FMT holds x in ((A \/ B) ^Fodelta ) implies x in ((A ^Fodelta ) \/ (B ^Fodelta ))

      proof

        let x be Element of FMT;

        assume

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

        

         A3: for W1 be Subset of FMT st W1 in ( U_FMT x) holds (W1 meets A & W1 meets (A ` ) or W1 meets B & W1 meets (B ` ))

        proof

          let W1 be Subset of FMT;

          assume

           A4: W1 in ( U_FMT x);

          then W1 meets ((A \/ B) ` ) by A2, Th19;

          then (W1 /\ ((A \/ B) ` )) <> {} ;

          then

           A5: (W1 /\ ((A ` ) /\ (B ` ))) <> {} by XBOOLE_1: 53;

          then ((W1 /\ (A ` )) /\ (B ` )) <> {} by XBOOLE_1: 16;

          then (W1 /\ (A ` )) meets (B ` );

          then

           A6: ex z1 be object st z1 in ((W1 /\ (A ` )) /\ (B ` )) by XBOOLE_0: 4;

          ((W1 /\ (B ` )) /\ (A ` )) <> {} by A5, XBOOLE_1: 16;

          then (W1 /\ (B ` )) meets (A ` );

          then

           A7: ex z2 be object st z2 in ((W1 /\ (B ` )) /\ (A ` )) by XBOOLE_0: 4;

          W1 meets (A \/ B) by A2, A4, Th19;

          then (W1 /\ (A \/ B)) <> {} ;

          then ((W1 /\ A) \/ (W1 /\ B)) <> {} by XBOOLE_1: 23;

          then (W1 /\ A) <> {} & (W1 /\ (A ` )) <> {} or (W1 /\ B) <> {} & (W1 /\ (B ` )) <> {} by A6, A7;

          hence thesis;

        end;

        for V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds V1 meets A & V1 meets (A ` ) or V2 meets B & V2 meets (B ` )

        proof

          let V1,V2 be Subset of FMT;

          assume V1 in ( U_FMT x) & V2 in ( U_FMT x);

          then

          consider W be Subset of FMT such that

           A8: W in ( U_FMT x) and

           A9: W c= (V1 /\ V2) by A1;

          (V1 /\ V2) c= V2 by XBOOLE_1: 17;

          then W c= V2 by A9;

          then

           A10: (W /\ B) c= (V2 /\ B) & (W /\ (B ` )) c= (V2 /\ (B ` )) by XBOOLE_1: 26;

          (V1 /\ V2) c= V1 by XBOOLE_1: 17;

          then W c= V1 by A9;

          then

           A11: (W /\ A) c= (V1 /\ A) & (W /\ (A ` )) c= (V1 /\ (A ` )) by XBOOLE_1: 26;

          V1 meets A & V1 meets (A ` ) or V2 meets B & V2 meets (B ` )

          proof

            now

              per cases by A3, A8;

                case W meets A & W meets (A ` );

                then (ex z1 be object st z1 in (W /\ A)) & ex z2 be object st z2 in (W /\ (A ` )) by XBOOLE_0: 4;

                hence thesis by A11;

              end;

                case W meets B & W meets (B ` );

                then (ex z3 be object st z3 in (W /\ B)) & ex z4 be object st z4 in (W /\ (B ` )) by XBOOLE_0: 4;

                hence thesis by A10;

              end;

            end;

            hence thesis;

          end;

          hence thesis;

        end;

        then (for V1 be Subset of FMT st V1 in ( U_FMT x) holds (V1 meets A & V1 meets (A ` ))) or for V2 be Subset of FMT st V2 in ( U_FMT x) holds V2 meets B & V2 meets (B ` );

        then x in (A ^Fodelta ) or x in (B ^Fodelta );

        hence thesis by XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO2:33

    for FMT be non empty FMT_Space_Str st FMT is Fo_filled holds (for A,B be Subset of FMT holds ((A \/ B) ^Fodelta ) = ((A ^Fodelta ) \/ (B ^Fodelta ))) implies for x be Element of FMT, V1,V2 be Subset of FMT st V1 in ( U_FMT x) & V2 in ( U_FMT x) holds ex W be Subset of FMT st W in ( U_FMT x) & W c= (V1 /\ V2)

    proof

      let FMT be non empty FMT_Space_Str;

      assume

       A1: FMT is Fo_filled;

      (ex x be Element of FMT, V1,V2 be Subset of FMT st (V1 in ( U_FMT x)) & (V2 in ( U_FMT x)) & (for W be Subset of FMT st W in ( U_FMT x) holds ( not (W c= (V1 /\ V2))))) implies ex A,B be Subset of FMT st ((A \/ B) ^Fodelta ) <> ((A ^Fodelta ) \/ (B ^Fodelta ))

      proof

        given x0 be Element of FMT, V1,V2 be Subset of FMT such that

         A2: V1 in ( U_FMT x0) and

         A3: V2 in ( U_FMT x0) and

         A4: for W be Subset of FMT st W in ( U_FMT x0) holds not W c= (V1 /\ V2);

        take (V1 ` ), (V2 ` );

        

         A5: not x0 in ((V2 ` ) ^Fodelta )

        proof

          assume x0 in ((V2 ` ) ^Fodelta );

          then V2 meets (V2 ` ) by A3, Th19;

          hence contradiction by XBOOLE_1: 79;

        end;

        for W be Subset of FMT st W in ( U_FMT x0) holds W meets ((V1 ` ) \/ (V2 ` )) & W meets (((V1 ` ) \/ (V2 ` )) ` )

        proof

          let W be Subset of FMT;

          assume

           A6: W in ( U_FMT x0);

          then

           A7: not W c= (V1 /\ V2) by A4;

          

           A8: W meets ((V1 /\ V2) ` )

          proof

            assume (W /\ ((V1 /\ V2) ` )) = {} ;

            then (W \ (V1 /\ V2)) = {} by SUBSET_1: 13;

            hence contradiction by A7, XBOOLE_1: 37;

          end;

          x0 in V1 & x0 in V2 by A1, A2, A3;

          then

           A9: x0 in (V1 /\ V2) by XBOOLE_0:def 4;

          x0 in W by A1, A6;

          then (W /\ (((V1 /\ V2) ` ) ` )) <> {} by A9, XBOOLE_0:def 4;

          then W meets (((V1 /\ V2) ` ) ` );

          hence thesis by A8, XBOOLE_1: 54;

        end;

        then

         A10: x0 in (((V1 ` ) \/ (V2 ` )) ^Fodelta );

         not x0 in ((V1 ` ) ^Fodelta )

        proof

          assume x0 in ((V1 ` ) ^Fodelta );

          then V1 meets (V1 ` ) by A2, Th19;

          hence contradiction by XBOOLE_1: 79;

        end;

        hence thesis by A10, A5, XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    theorem :: FINTOPO2:34

    for x be Element of FMT, A be Subset of FMT holds x in (A ^Fos ) iff x in A & not x in ((A \ {x}) ^Fob )

    proof

      let x be Element of FMT;

      let A be Subset of FMT;

      

       A1: x in A & not x in ((A \ {x}) ^Fob ) implies x in (A ^Fos )

      proof

        assume that

         A2: x in A and

         A3: not x in ((A \ {x}) ^Fob );

        consider V9 be Subset of FMT such that

         A4: V9 in ( U_FMT x) and

         A5: V9 misses (A \ {x}) by A3;

        V9 misses (A /\ ( {x} ` )) by A5, SUBSET_1: 13;

        then (V9 /\ (A /\ ( {x} ` ))) = {} ;

        then ((V9 /\ ( {x} ` )) /\ A) = {} by XBOOLE_1: 16;

        then ((V9 \ {x}) /\ A) = {} by SUBSET_1: 13;

        then (V9 \ {x}) misses A;

        hence thesis by A2, A4;

      end;

      x in (A ^Fos ) implies x in A & not x in ((A \ {x}) ^Fob )

      proof

        assume

         A6: x in (A ^Fos );

        then

        consider V9 be Subset of FMT such that

         A7: V9 in ( U_FMT x) and

         A8: (V9 \ {x}) misses A by Th22;

        (V9 /\ ( {x} ` )) misses A by A8, SUBSET_1: 13;

        then ((V9 /\ ( {x} ` )) /\ A) = {} ;

        then (V9 /\ (( {x} ` ) /\ A)) = {} by XBOOLE_1: 16;

        then V9 misses (( {x} ` ) /\ A);

        then V9 misses (A \ {x}) by SUBSET_1: 13;

        hence thesis by A6, A7, Th20, Th22;

      end;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:35

    

     Th35: for FMT be non empty FMT_Space_Str holds FMT is Fo_filled iff for A be Subset of FMT holds A c= (A ^Fob )

    proof

      let FMT be non empty FMT_Space_Str;

      

       A1: (for A be Subset of FMT holds A c= (A ^Fob )) implies FMT is Fo_filled

      proof

        assume

         A2: for A be Subset of FMT holds A c= (A ^Fob );

        assume not FMT is Fo_filled;

        then

        consider y be Element of FMT, V be Subset of FMT such that

         A3: V in ( U_FMT y) and

         A4: not y in V;

        

         A5: V misses {y}

        proof

          assume V meets {y};

          then ex z be object st z in V & z in {y} by XBOOLE_0: 3;

          hence contradiction by A4, TARSKI:def 1;

        end;

         not {y} c= ( {y} ^Fob )

        proof

          

           A6: y in {y} by TARSKI:def 1;

          assume {y} c= ( {y} ^Fob );

          hence contradiction by A3, A5, A6, Th20;

        end;

        hence contradiction by A2;

      end;

      FMT is Fo_filled implies for A be Subset of FMT holds A c= (A ^Fob )

      proof

        assume

         A7: FMT is Fo_filled;

        let A be Subset of FMT;

        let x be object;

        assume

         A8: x in A;

        then

        reconsider y = x as Element of FMT;

        for W be Subset of FMT st W in ( U_FMT y) holds W meets A

        proof

          let W be Subset of FMT;

          assume W in ( U_FMT y);

          then y in W by A7;

          hence thesis by A8, XBOOLE_0: 3;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:36

    

     Th36: for FMT be non empty FMT_Space_Str holds FMT is Fo_filled iff for A be Subset of FMT holds (A ^Foi ) c= A

    proof

      let FMT be non empty FMT_Space_Str;

      

       A1: FMT is Fo_filled implies for A be Subset of FMT holds (A ^Foi ) c= A

      proof

        assume

         A2: FMT is Fo_filled;

        let A be Subset of FMT;

        let x be object;

        assume

         A3: x in (A ^Foi );

        then

        reconsider y = x as Element of FMT;

        consider V be Subset of FMT such that

         A4: V in ( U_FMT y) and

         A5: V c= A by A3, Th21;

        y in V by A2, A4;

        hence thesis by A5;

      end;

      (for A be Subset of FMT holds (A ^Foi ) c= A) implies FMT is Fo_filled

      proof

        assume

         A6: for A be Subset of FMT holds (A ^Foi ) c= A;

        assume not FMT is Fo_filled;

        then

        consider y be Element of FMT, V be Subset of FMT such that

         A7: V in ( U_FMT y) and

         A8: not y in V;

        y in (V ^Foi ) by A7;

        then not (V ^Foi ) c= V by A8;

        hence contradiction by A6;

      end;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:37

    

     Th37: (((A ` ) ^Fob ) ` ) = (A ^Foi )

    proof

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

      proof

        let x be object;

        thus x in (((A ` ) ^Fob ) ` ) implies x in (A ^Foi )

        proof

          assume

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

          then

          reconsider y = x as Element of FMT;

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

          then

          consider V be Subset of FMT such that

           A2: V in ( U_FMT y) and

           A3: V misses (A ` );

          (V /\ (A ` )) = {} by A3;

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

          then V c= A by XBOOLE_1: 37;

          hence thesis by A2;

        end;

        assume

         A4: x in (A ^Foi );

        then

        reconsider y = x as Element of FMT;

        consider V be Subset of FMT such that

         A5: V in ( U_FMT y) and

         A6: V c= A by A4, Th21;

        (V \ A) = {} by A6, XBOOLE_1: 37;

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

        then V misses (A ` );

        then not y in ((A ` ) ^Fob ) by A5, Th20;

        hence thesis by XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINTOPO2:38

    

     Th38: (((A ` ) ^Foi ) ` ) = (A ^Fob )

    proof

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

      proof

        let x be object;

        thus x in (((A ` ) ^Foi ) ` ) implies x in (A ^Fob )

        proof

          assume

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

          then

          reconsider y = x as Element of FMT;

          

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

          for W be Subset of FMT st W in ( U_FMT y) holds W meets A

          proof

            let W be Subset of FMT;

            assume W in ( U_FMT y);

            then not W c= (A ` ) by A2;

            then

            consider z be object such that

             A3: z in W and

             A4: not z in (A ` );

            z in A by A3, A4, XBOOLE_0:def 5;

            hence thesis by A3, XBOOLE_0: 3;

          end;

          hence thesis;

        end;

        assume

         A5: x in (A ^Fob );

        then

        reconsider y = x as Element of FMT;

        for W be Subset of FMT st W in ( U_FMT y) holds not W c= (A ` )

        proof

          let W be Subset of FMT;

          assume W in ( U_FMT y);

          then W meets A by A5, Th20;

          then ex z be object st z in W & z in A by XBOOLE_0: 3;

          hence thesis by XBOOLE_0:def 5;

        end;

        then not y in ((A ` ) ^Foi ) by Th21;

        hence thesis by XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINTOPO2:39

    

     Th39: (A ^Fodelta ) = ((A ^Fob ) /\ ((A ` ) ^Fob ))

    proof

      for x be Element of FMT holds x in (A ^Fodelta ) iff x in ((A ^Fob ) /\ ((A ` ) ^Fob ))

      proof

        let x be Element of FMT;

        thus x in (A ^Fodelta ) implies x in ((A ^Fob ) /\ ((A ` ) ^Fob ))

        proof

          assume

           A1: x in (A ^Fodelta );

          then for W be Subset of FMT st W in ( U_FMT x) holds W meets (A ` ) by Th19;

          then

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

          for W be Subset of FMT st W in ( U_FMT x) holds W meets A by A1, Th19;

          then x in (A ^Fob );

          hence thesis by A2, XBOOLE_0:def 4;

        end;

        assume x in ((A ^Fob ) /\ ((A ` ) ^Fob ));

        then x in (A ^Fob ) & x in ((A ` ) ^Fob ) by XBOOLE_0:def 4;

        then for W be Subset of FMT st W in ( U_FMT x) holds W meets A & W meets (A ` ) by Th20;

        hence thesis;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: FINTOPO2:40

    (A ^Fodelta ) = ((A ^Fob ) /\ ((A ^Foi ) ` ))

    proof

      (((A ` ) ^Fob ) ` ) = (A ^Foi ) by Th37;

      hence thesis by Th39;

    end;

    theorem :: FINTOPO2:41

    (A ^Fodelta ) = ((A ` ) ^Fodelta )

    proof

      (A ^Fodelta ) = ((((A ` ) ` ) ^Fob ) /\ ((A ` ) ^Fob )) by Th39;

      hence thesis by Th39;

    end;

    theorem :: FINTOPO2:42

    (A ^Fodelta ) = ((A ^Fob ) \ (A ^Foi ))

    proof

      for x be object holds x in (A ^Fodelta ) iff x in ((A ^Fob ) \ (A ^Foi ))

      proof

        let x be object;

        thus x in (A ^Fodelta ) implies x in ((A ^Fob ) \ (A ^Foi ))

        proof

          assume x in (A ^Fodelta );

          then x in ((A ^Fob ) /\ ((((A ` ) ^Fob ) ` ) ` )) by Th39;

          then x in ((A ^Fob ) /\ ((A ^Foi ) ` )) by Th37;

          hence thesis by SUBSET_1: 13;

        end;

        assume x in ((A ^Fob ) \ (A ^Foi ));

        then x in ((A ^Fob ) /\ ((A ^Foi ) ` )) by SUBSET_1: 13;

        then x in ((A ^Fob ) /\ ((((A ` ) ^Fob ) ` ) ` )) by Th37;

        hence thesis by Th39;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let FMT;

      let A;

      :: FINTOPO2:def14

      func A ^Fodel_i -> Subset of FMT equals (A /\ (A ^Fodelta ));

      coherence ;

      :: FINTOPO2:def15

      func A ^Fodel_o -> Subset of FMT equals ((A ` ) /\ (A ^Fodelta ));

      coherence ;

    end

    theorem :: FINTOPO2:43

    (A ^Fodelta ) = ((A ^Fodel_i ) \/ (A ^Fodel_o ))

    proof

      for x be object holds x in (A ^Fodelta ) iff x in ((A ^Fodel_i ) \/ (A ^Fodel_o ))

      proof

        let x be object;

        thus x in (A ^Fodelta ) implies x in ((A ^Fodel_i ) \/ (A ^Fodel_o ))

        proof

          assume x in (A ^Fodelta );

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

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

          hence thesis by XBOOLE_1: 23;

        end;

        assume x in ((A ^Fodel_i ) \/ (A ^Fodel_o ));

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

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

        hence thesis by XBOOLE_1: 28;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let FMT;

      let G be Subset of FMT;

      :: FINTOPO2:def16

      attr G is Fo_open means G = (G ^Foi );

      :: FINTOPO2:def17

      attr G is Fo_closed means G = (G ^Fob );

    end

    theorem :: FINTOPO2:44

    (A ` ) is Fo_open implies A is Fo_closed

    proof

      assume (A ` ) is Fo_open;

      then

       A1: (A ` ) = ((A ` ) ^Foi );

      ((((A ` ) ^Foi ) ` ) ` ) = ((A ^Fob ) ` ) by Th38;

      hence thesis by A1;

    end;

    theorem :: FINTOPO2:45

    (A ` ) is Fo_closed implies A is Fo_open

    proof

      assume (A ` ) is Fo_closed;

      then

       A1: (A ` ) = ((A ` ) ^Fob );

      ((A ` ) ^Fob ) = ((((A ` ) ` ) ^Foi ) ` ) by Th38

      .= ((A ^Foi ) ` );

      

      then A = (((A ^Foi ) ` ) ` ) by A1

      .= (A ^Foi );

      hence thesis;

    end;

    theorem :: FINTOPO2:46

    for FMT be non empty FMT_Space_Str, A,B be Subset of FMT st FMT is Fo_filled holds (for x be Element of FMT holds {x} in ( U_FMT x)) implies ((A /\ B) ^Fob ) = ((A ^Fob ) /\ (B ^Fob ))

    proof

      let FMT be non empty FMT_Space_Str;

      let A,B be Subset of FMT;

      assume

       A1: FMT is Fo_filled;

      assume

       A2: for x be Element of FMT holds {x} in ( U_FMT x);

      

       A3: for C be Subset of FMT holds (C ^Fob ) c= C

      proof

        let C be Subset of FMT;

        for y be Element of FMT holds y in (C ^Fob ) implies y in C

        proof

          let y be Element of FMT;

          assume

           A4: y in (C ^Fob );

           {y} in ( U_FMT y) by A2;

          then {y} meets C by A4, Th20;

          then ex z be object st z in {y} & z in C by XBOOLE_0: 3;

          hence thesis by TARSKI:def 1;

        end;

        hence thesis;

      end;

      

       A5: for C be Subset of FMT holds (C ^Fob ) = C by A1, A3, Th35;

      then ((A /\ B) ^Fob ) = (A /\ B) & (A ^Fob ) = A;

      hence thesis by A5;

    end;

    theorem :: FINTOPO2:47

    for FMT be non empty FMT_Space_Str, A,B be Subset of FMT st FMT is Fo_filled holds (for x be Element of FMT holds {x} in ( U_FMT x)) implies ((A ^Foi ) \/ (B ^Foi )) = ((A \/ B) ^Foi )

    proof

      let FMT be non empty FMT_Space_Str;

      let A,B be Subset of FMT;

      assume

       A1: FMT is Fo_filled;

      assume

       A2: for x be Element of FMT holds {x} in ( U_FMT x);

      

       A3: for C be Subset of FMT holds C c= (C ^Foi )

      proof

        let C be Subset of FMT;

        for y be Element of FMT holds y in C implies y in (C ^Foi )

        proof

          let y be Element of FMT;

          assume y in C;

          then

           A4: {y} is Subset of C by SUBSET_1: 41;

           {y} in ( U_FMT y) by A2;

          hence thesis by A4;

        end;

        hence thesis;

      end;

      

       A5: for C be Subset of FMT holds C = (C ^Foi ) by A1, A3, Th36;

      then ((A \/ B) ^Foi ) = (A \/ B) & (A ^Foi ) = A;

      hence thesis by A5;

    end;