FINTOPO2

:: Formal topological spaces
::  by Gang Liu , Yasushi Fuwa and Masayoshi Eguchi
::
:: Received October 13, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, ORDERS_2, SUBSET_1, TARSKI, FIN_TOPO, RCOMP_1,
      MARGREL1, XBOOLEAN, STRUCT_0, FUNCT_1, ZFMISC_1, PRE_TOPC, SETFAM_1,
      FINTOPO2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, FUNCT_1,
      FUNCT_2, FIN_TOPO, ORDERS_2, PRE_TOPC, MARGREL1;
 constructors DOMAIN_1, MARGREL1, PRE_TOPC, FIN_TOPO, RELSET_1, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, FIN_TOPO;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions TARSKI, STRUCT_0, XBOOLE_0;
 equalities SUBSET_1, XBOOLEAN, FIN_TOPO;
 expansions TARSKI, XBOOLE_0, FIN_TOPO;
 theorems TARSKI, SUBSET_1, FIN_TOPO, FUNCT_2, XBOOLE_0, XBOOLE_1;
 schemes DOMAIN_1, FUNCT_2;

begin

::
::     SECTION1 : Some Useful Theorems on Finite Topological Spaces
::

reserve FT for non empty RelStr;
reserve A for Subset of FT;

theorem
  for FT being non empty RelStr, A,B being 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 being 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 Th2:
  A^delta = (A^b) /\ ((A^i)`)
proof
  for x being 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
  A^delta = A^b \ A^i
proof
  for x being 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
  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
  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;
  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;
  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
  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
  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 Th8:
  for x be Element of FT, A be Subset of FT holds x in A^delta iff
  ex y1,y2 being 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 being 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 being 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 being 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;
  func P_0(x,y) -> Element of BOOLEAN equals
  :Def3:
  TRUE if y in U_FT x
  otherwise FALSE;
  correctness;
end;

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

theorem
  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
  for x be Element of FT, A be Subset of FT holds x in A^b iff ex y1
  being 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 being 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 being 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;
  func P_A(x,A) -> Element of BOOLEAN equals
  :Def4:
  TRUE if x in A otherwise
  FALSE;
  correctness;
end;

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

theorem
  for x be Element of FT, A be Subset of FT holds x in A^deltai iff (ex
y1,y2 being 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 being 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 being 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 being 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
  for x be Element of FT, A be Subset of FT holds x in A^deltao iff (ex
y1,y2 being 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 being 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 being 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 being 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;
  func P_e(x,y) -> Element of BOOLEAN equals
  :Def5:
  TRUE if x = y otherwise
  FALSE;
  correctness;
end;

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

theorem
  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 being 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 being 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 being Element of FT st P_1(x,y,A)=TRUE & P_e(x,y)=FALSE )
    proof
      given y being 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 being 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 being 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
  for x be Element of FT, A be Subset of FT holds x in A^n iff P_A(x,A)=
  TRUE & ex y being 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 being 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 being 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 being 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 being Element of FT st P_1(x,y,A)=TRUE & P_e(x,y)=FALSE;
    consider y being 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
  for x be Element of FT, A be Subset of FT holds x in A^f iff ex y
  being 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 being Element of FT st P_A(y,A)=TRUE & P_0(y,x)=TRUE) implies x in
  A^f
  proof
    assume ex y being Element of FT st P_A(y,A)=TRUE & P_0(y,x)=TRUE;
    then consider y being 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 being Element of FT st P_A(y,A)=TRUE & P_0(y,x)= TRUE
  proof
    assume x in A^f;
    then consider y being 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

::
::          SECTION2: Formal Topological Spaces
::

definition
  struct ( 1-sorted ) FMT_Space_Str (# carrier -> set, BNbd -> Function of the
    carrier, bool bool the carrier #);
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;
  func U_FMT x -> Subset-Family of FMT equals
  ( the BNbd of FMT ).x;
  correctness;
end;

definition
  let T;
  func NeighSp T -> non empty strict FMT_Space_Str means
  the carrier of it =
the carrier of T & for x being Point of it holds U_FMT x = {V where V is Subset
  of T: V in the topology of T & x in V};
  existence
  proof
    ex IT being non empty strict FMT_Space_Str st the carrier of IT = the
carrier of T & for x being Point of IT holds U_FMT x = {V where V is Subset of
T:  V in the topology of T & x in V}
    proof
      deffunc F(set) = {V where V is Subset of T: V in the topology of T & $1
      in V};
A1:   for x being Element of T holds F(x) in bool bool the carrier of T
      proof
        let x being Element of T;
        now
          let Y be object;
          assume
          Y in {V where V is Subset of T: V in the topology of T & x in V};
          then ex V being 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 is 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 being 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 being Point of it1 holds U_FMT x = {V where V is 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 being Point of it2 holds U_FMT x = {V where V is Subset of
T:  V in the topology of T & x in V};
A7: for x being Element of it2 holds (the BNbd of it2).x = {V where V is
    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 being Element of it1 holds (the BNbd of it1).x = {V where V is
    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 being Point of it1;
      thus (the BNbd of it1).x = {V where V is 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;
  attr IT is Fo_filled means

  for x being Element of IT for D being
  Subset of IT st D in U_FMT x holds x in D;
end;

definition
  let FMT;
  let A;
  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 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;
  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 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;
  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 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;
  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 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;
  func A^Fon -> Subset of FMT equals
  A\(A^Fos);
  coherence;
end;

theorem
  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 Th24:
  for FMT being non empty FMT_Space_Str, A, B being 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 being 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 being 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 Th25:
  for FMT being non empty FMT_Space_Str, A,B being 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 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
  (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
  ((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 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
  for FMT being non empty FMT_Space_Str holds (for x being Element of
FMT, V1,V2 being Subset of FMT st ((V1 in U_FMT x) & (V2 in U_FMT x)) holds ex
  W being Subset of FMT st ((W in U_FMT x) & (W c= (V1 /\ V2)))) iff for A,B
  being Subset of FMT holds (A \/ B)^Fob = ((A^Fob) \/ (B^Fob))
proof
  let FMT be non empty FMT_Space_Str;
A1: (for x being Element of FMT, V1,V2 being Subset of FMT st ((V1 in U_FMT
x) & (V2 in U_FMT x)) holds ex W being Subset of FMT st ((W in U_FMT x) & (W c=
(V1 /\ V2)))) implies for A,B being Subset of FMT holds (A \/ B)^Fob = ((A^Fob)
  \/ (B^Fob))
  proof
    assume
A2: for x being Element of FMT, V1,V2 being Subset of FMT st V1 in
U_FMT x & V2 in U_FMT x holds ex W being 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 being Subset of FMT st W1 in U_FMT x holds W1 meets A or W1
        meets B
        proof
          let W1 being 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 being 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 being 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 being 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 being Subset of FMT st V1 in U_FMT x holds V1 meets A) or
        for V2 being 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 being Element of FMT, V1,V2 being Subset of FMT st (V1 in U_FMT x
  ) & (V2 in U_FMT x) & (for W being Subset of FMT st W in U_FMT x holds (not(W
  c= V1 /\ V2)) ) ) implies ex A,B being Subset of FMT st ((A \/ B)^Fob) <> ((A
  ^Fob) \/ (B^Fob))
  proof
    given x0 being Element of FMT, V1,V2 being Subset of FMT such that
A11: V1 in U_FMT x0 and
A12: V2 in U_FMT x0 and
A13: for W being 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 being Subset of FMT st W in U_FMT x0 holds W meets ((V1)` \/ ( V2)`)
    proof
      let W being 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
  for FMT being non empty FMT_Space_Str holds (for x being Element of
  FMT, V1,V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W
being Subset of FMT st (W in U_FMT x & W c= V1 /\ V2)) iff for A,B being Subset
  of FMT holds (A^Foi) /\ (B^Foi) = (A /\ B)^Foi
proof
  let FMT be non empty FMT_Space_Str;
  thus (for x being Element of FMT, V1,V2 being Subset of FMT st V1 in U_FMT x
& V2 in U_FMT x holds ex W being Subset of FMT st (W in U_FMT x & W c= V1 /\ V2
)) implies for A,B being Subset of FMT holds (A^Foi) /\ (B^Foi) = (A /\ B)^Foi
  proof
    assume
A1: for x being Element of FMT, V1,V2 being Subset of FMT st V1 in
U_FMT x & V2 in U_FMT x holds ex W being 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 being 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 being Subset of FMT st W1 in U_FMT x & W1 c= A by Th21;
        then consider W1,W2 being 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 being 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 being Element of FMT, V1,V2 being Subset of FMT st (V1 in U_FMT x
  & V2 in U_FMT x) & (for W being Subset of FMT st W in U_FMT x holds (not(W c=
V1 /\ V2)) ) ) implies ex A,B being Subset of FMT st ((A^Foi) /\ (B^Foi)) <> (A
  /\ B)^Foi
  proof
    given x0 being Element of FMT, V1,V2 being Subset of FMT such that
A12: V1 in U_FMT x0 & V2 in U_FMT x0 and
A13: for W being 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 being Subset of FMT holds ((A^Foi) /\ (B^Foi)) = (A /\ B) ^Foi
) implies for x being Element of FMT, V1,V2 being Subset of FMT st V1 in U_FMT
  x & V2 in U_FMT x holds ex W being Subset of FMT st W in U_FMT x & W c= V1 /\
  V2;
end;

theorem
  for FMT being non empty FMT_Space_Str, A,B being Subset of FMT holds (
for x being Element of FMT, V1,V2 being Subset of FMT st ((V1 in U_FMT x) & V2
in U_FMT x) holds ex W being 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 being Element of FMT, V1,V2 being Subset of FMT st V1 in U_FMT
  x & V2 in U_FMT x holds ex W being 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 being 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 being 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 being 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 being 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 being 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 being 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 being object st z1 in W /\ A )&
ex z2 being 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 being object st z3 in W /\ B )&
ex z4 being 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 being Subset of FMT st V1 in U_FMT x holds (V1 meets A & V1
meets A`)) or for V2 being 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
  for FMT being non empty FMT_Space_Str st FMT is Fo_filled holds (for A
  ,B being Subset of FMT holds (A \/ B)^Fodelta = ((A^Fodelta) \/ (B^Fodelta)))
implies for x being Element of FMT, V1,V2 being Subset of FMT st V1 in U_FMT x
& V2 in U_FMT x holds ex W being 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 being Element of FMT, V1,V2 being Subset of FMT st (V1 in U_FMT x)
& (V2 in U_FMT x) & (for W being Subset of FMT st W in U_FMT x holds (not(W c=
V1 /\ V2)) ) ) implies ex A,B being Subset of FMT st ((A \/ B)^Fodelta) <> ((A
  ^Fodelta) \/ (B^Fodelta))
  proof
    given x0 being Element of FMT, V1,V2 being Subset of FMT such that
A2: V1 in U_FMT x0 and
A3: V2 in U_FMT x0 and
A4: for W being 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 being Subset of FMT st W in U_FMT x0 holds W meets ((V1)` \/ (V2
    )`) & W meets ((V1)` \/ (V2)`)`
    proof
      let W being 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
  for x be Element of FMT, A being 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 being 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 being 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 Th35:
  for FMT being non empty FMT_Space_Str holds FMT is Fo_filled iff
  for A being Subset of FMT holds A c= A^Fob
proof
  let FMT be non empty FMT_Space_Str;
A1: (for A being Subset of FMT holds A c= A^Fob) implies FMT is Fo_filled
  proof
    assume
A2: for A being Subset of FMT holds A c= A^Fob;
    assume not FMT is Fo_filled;
    then consider y being Element of FMT, V being 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 being 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 being Subset of FMT holds A c= A^Fob
  proof
    assume
A7: FMT is Fo_filled;
    let A being Subset of FMT;
    let x be object;
    assume
A8: x in A;
    then reconsider y=x as Element of FMT;
    for W being 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 Th36:
  for FMT being non empty FMT_Space_Str holds FMT is Fo_filled iff
  for A being 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 being 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 being Subset of FMT holds A^Foi c= A) implies FMT is Fo_filled
  proof
    assume
A6: for A being Subset of FMT holds A^Foi c= A;
    assume not FMT is Fo_filled;
    then consider y being Element of FMT, V being 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 Th37:
  ((A`)^Fob)` =A^Foi
proof
  for x being 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 Th38:
  ((A`)^Foi)` = A^Fob
proof
  for x being 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 being 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 being 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 being 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 being 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 Th39:
  A^Fodelta = (A^Fob) /\ ((A`)^Fob)
proof
  for x being 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 being Subset of FMT st W in U_FMT x holds W meets A` by Th19;
      then
A2:   x in((A`)^Fob);
      for W being 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 being 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
  A^Fodelta = (A^Fob) /\ (A^Foi)`
proof
  ((A`)^Fob)`= A^Foi by Th37;
  hence thesis by Th39;
end;

theorem
  A^Fodelta = (A`)^Fodelta
proof
  A^Fodelta = (((A`)`)^Fob) /\ ((A`)^Fob) by Th39;
  hence thesis by Th39;
end;

theorem
  A^Fodelta = A^Fob \ A^Foi
proof
  for x being 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;
  func A^Fodel_i -> Subset of FMT equals
  A /\ (A^Fodelta);
  coherence;
  func A^Fodel_o -> Subset of FMT equals
  A` /\ (A^Fodelta);
  coherence;
end;

theorem
  A^Fodelta = (A^Fodel_i) \/ (A^Fodel_o)
proof
  for x being 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;
  attr G is Fo_open means

  G = G^Foi;
  attr G is Fo_closed means

  G = G^Fob;
end;

theorem
  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
  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
  for FMT being non empty FMT_Space_Str, A,B being Subset of FMT st FMT
is Fo_filled holds (for x being 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 being Element of FMT holds {x} in U_FMT x;
A3: for C being Subset of FMT holds C^Fob c= C
  proof
    let C be Subset of FMT;
    for y being 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 being 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 being 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
  for FMT being non empty FMT_Space_Str, A,B being Subset of FMT st FMT
is Fo_filled holds (for x being 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 being Element of FMT holds {x} in U_FMT x;
A3: for C being Subset of FMT holds C c= C^Foi
  proof
    let C be Subset of FMT;
    for y being 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 being 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;