The Mizar article:

On the Characterizations of Compactness

by
Grzegorz Bancerek,
Noboru Endou, and
Yuji Sakai

Received July 29, 2001

Copyright (c) 2001 Association of Mizar Users

MML identifier: YELLOW19
[ MML identifier index ]


environ

 vocabulary YELLOW_1, ORDERS_1, WELLORD2, COLLSP, FILTER_0, LATTICES, BOOLE,
      PRE_TOPC, SUBSET_1, CONNSP_2, WAYBEL_0, TOPS_1, WAYBEL_7, RELAT_1,
      RELAT_2, FUNCT_1, FINSET_1, SETFAM_1, QUANTAL1, LATTICE3, ORDINAL2,
      MCART_1, YELLOW_6, SEQ_2, SUB_METR, CANTOR_1, COMPTS_1, OPPCAT_1,
      ARYTM_3, CLASSES1, YELLOW_0, CAT_1, BHSP_3, YELLOW19;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MCART_1, SETFAM_1,
      FINSET_1, FUNCT_1, RELAT_2, RELSET_1, FUNCT_2, CLASSES1, STRUCT_0,
      PRE_TOPC, TOPS_1, TOPS_2, TEX_2, COMPTS_1, CONNSP_2, CANTOR_1, ORDERS_1,
      LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, YELLOW_6, WAYBEL_9,
      YELLOW_7, WAYBEL32;
 constructors TOLER_1, RELAT_2, WAYBEL_1, CLASSES1, TOPS_1, TOPS_2, CONNSP_2,
      CANTOR_1, WAYBEL_7, WAYBEL32, TEX_2, REALSET1, MEMBERED;
 clusters SUBSET_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, PUA2MSS1, RELSET_1,
      RLVECT_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, WAYBEL_9,
      YELLOW_6, WAYBEL32, MEMBERED, RELAT_1, ZFMISC_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, TOPS_2, COMPTS_1, WAYBEL_0, WAYBEL_7, WAYBEL_9, XBOOLE_0;
 theorems TARSKI, SETFAM_1, FUNCT_2, FINSET_1, FUNCT_1, CLASSES1, RELAT_1,
      ZFMISC_1, MCART_1, RELAT_2, SUBSET_1, PRE_TOPC, TOPS_1, TOPS_2, TEX_2,
      COMPTS_1, CONNSP_2, CANTOR_1, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0,
      YELLOW_1, WAYBEL_7, WAYBEL_8, WAYBEL_9, YELLOW_5, YELLOW_6, YELLOW_7,
      WAYBEL12, WAYBEL21, WAYBEL32, XBOOLE_0, XBOOLE_1;
 schemes RELSET_1, FUNCT_2, COMPTS_1;

begin

reserve x,y,X for set;

canceled;

theorem Th2:
 for X being non empty set
 for F being proper Filter of BoolePoset X
 for A being set st A in F
  holds A is not empty
  proof let X be non empty set;
      Bottom BoolePoset X = {} by YELLOW_1:18;
   hence thesis by WAYBEL_7:8;
  end;

definition
 let T be non empty TopSpace;
 let x be Point of T;
 func NeighborhoodSystem x -> Subset of BoolePoset [#]T equals:
Def1:
  {A where A is a_neighborhood of x: not contradiction};
 coherence
  proof set X = the carrier of T;
   set Y = {A where A is a_neighborhood of x: not contradiction};
A1: the carrier of BoolePoset X = bool X by WAYBEL_7:4;
A2: X = [#]T by PRE_TOPC:12;
      Y c= bool X
     proof let y being set; assume y in Y;
       then ex A being a_neighborhood of x st y = A;
      hence thesis;
     end;
   hence thesis by A1,A2;
  end;
end;

theorem Th3:
 for T being non empty TopSpace, x being Point of T, A being set
  holds A in NeighborhoodSystem x iff A is a_neighborhood of x
   proof let T be non empty TopSpace, x be Point of T, B be set;
    defpred P[] means not contradiction;
       NeighborhoodSystem x = {A where A is a_neighborhood of x: P[]} by Def1
;
     then B in NeighborhoodSystem x iff ex A being a_neighborhood of x st B =
A;
    hence thesis;
   end;

definition
 let T be non empty TopSpace;
 let x be Point of T;
 cluster NeighborhoodSystem x -> non empty proper upper filtered;
 coherence
  proof consider A0 being a_neighborhood of x;
      A0 in NeighborhoodSystem x by Th3;
   hence NeighborhoodSystem x is non empty;
   set X = the carrier of T, L = BoolePoset [#]T;
   set Y = NeighborhoodSystem x;
A1: the carrier of BoolePoset X = bool X by WAYBEL_7:4;
A2: X = [#]T by PRE_TOPC:12;
A3:  {} is not a_neighborhood of x by CONNSP_2:6;
      {} c= X by XBOOLE_1:2;
    then {} in bool X & not {} in NeighborhoodSystem x by A3,Th3;
   hence NeighborhoodSystem x is proper by A1,A2,TEX_2:5;
   thus NeighborhoodSystem x is upper
     proof let a,b be Element of L; assume a in Y;
      then reconsider A = a as a_neighborhood of x by Th3;
      reconsider B = b as Subset of T by A1,A2;
      assume a <= b; then A c= B by YELLOW_1:2;
       then Int A c= Int B & x in Int A by CONNSP_2:def 1,TOPS_1:48;
       then b is a_neighborhood of x by CONNSP_2:def 1;
      hence thesis by Th3;
     end;
   let a,b be Element of L; assume a in Y & b in Y;
   then reconsider A = a, B = b as a_neighborhood of x by Th3;
    A4: A /\ B is a_neighborhood of x by CONNSP_2:4;
then A /\ B in NeighborhoodSystem x by Th3;
   then reconsider z = A /\ B as Element of L;
   take z; z c= A & z c= B by XBOOLE_1:17;
   hence thesis by A4,Th3,YELLOW_1:2;
  end;
end;

theorem Th4:
 for T being non empty TopSpace, x being Point of T
 for F being upper Subset of BoolePoset [#]T holds
   x is_a_convergence_point_of F, T iff NeighborhoodSystem x c= F
  proof let T be non empty TopSpace, x be Point of T;
A1: the carrier of T = [#]T by PRE_TOPC:12;
   let F be upper Subset of BoolePoset [#]T;
   hereby assume
A2:   x is_a_convergence_point_of F, T;
     thus NeighborhoodSystem x c= F
       proof let y; assume y in NeighborhoodSystem x;
        then reconsider y as a_neighborhood of x by Th3;
           x in Int y by CONNSP_2:def 1;
         then Int y in F & Int y c= y by A2,TOPS_1:44,WAYBEL_7:def 5;
        hence thesis by A1,WAYBEL_7:11;
       end;
    end;
   assume
A3: NeighborhoodSystem x c= F;
   let A be Subset of T; assume A is open & x in A;
    then A is a_neighborhood of x by CONNSP_2:5;
    then A in NeighborhoodSystem x by Th3;
   hence thesis by A3;
  end;

theorem
   for T being non empty TopSpace, x being Point of T
  holds x is_a_convergence_point_of NeighborhoodSystem x, T by Th4;

theorem
   for T being non empty TopSpace
 for A being Subset of T holds
  A is open iff
    for x being Point of T st x in A
    for F being Filter of BoolePoset [#]T
     st x is_a_convergence_point_of F, T
     holds A in F
  proof let T be non empty TopSpace, A be Subset of T;
   thus A is open implies
    for x being Point of T st x in A
    for F being Filter of BoolePoset [#]T
     st x is_a_convergence_point_of F, T
     holds A in F by WAYBEL_7:def 5;
   assume
A1: for x being Point of T st x in A
    for F being Filter of BoolePoset [#]T
     st x is_a_convergence_point_of F, T
     holds A in F;
   consider x being Element of A \ Int A;
   assume A is not open;
    then A <> Int A & Int A c= A by TOPS_1:44;
    then not A c= Int A by XBOOLE_0:def 10;
then A2: A \ Int A <> {} by XBOOLE_1:37;
    then x in A \ Int A;
   then reconsider x as Point of T;
      x is_a_convergence_point_of NeighborhoodSystem x, T &
    x in A by A2,Th4,XBOOLE_0:def 4;
    then A in NeighborhoodSystem x by A1;
    then A is a_neighborhood of x by Th3;
    then x in Int A by CONNSP_2:def 1;
   hence thesis by A2,XBOOLE_0:def 4;
  end;

definition
 let S be non empty 1-sorted;
 let N be non empty NetStr over S;
 mode Subset of S,N -> Subset of S means:
Def2:
  ex i being Element of N st it = rng the mapping of N|i;
 existence
  proof consider i being Element of N;
   reconsider A = rng the mapping of N|i as Subset of S;
   take A, i; thus thesis;
  end;
end;

theorem Th7:
 for S being non empty 1-sorted
 for N being non empty NetStr over S
 for i being Element of N
  holds rng the mapping of N|i is Subset of S, N by Def2;

definition
 let S be non empty 1-sorted;
 let N be reflexive non empty NetStr over S;
 cluster -> non empty Subset of S,N;
 coherence
  proof let A be Subset of S,N;
   consider i being Element of N such that
A1: A = rng the mapping of N|i by Def2;
   thus thesis by A1;
  end;
end;

theorem Th8:
 for S being non empty 1-sorted, N being net of S
 for i being Element of N, x being set holds
  x in rng the mapping of N|i iff
     ex j being Element of N st i <= j & x = N.j
  proof let S be non empty 1-sorted, N be net of S;
   let i be Element of N, x be set;
A1: dom the mapping of N|i = the carrier of N|i by FUNCT_2:def 1;
   hereby assume x in rng the mapping of N|i;
     then consider y being set such that
A2:   y in the carrier of N|i & x = (the mapping of N|i).y by A1,FUNCT_1:def 5;
     reconsider y as Element of N|i by A2;
     consider j being Element of N such that
A3:   j = y & i <= j by WAYBEL_9:def 7;
     take j; thus i <= j by A3;
     thus x = (N|i).y by A2,WAYBEL_0:def 8 .= N.j by A3,WAYBEL_9:16;
    end;
   given j being Element of N such that
A4: i <= j & x = N.j;
A5: j in the carrier of N|i by A4,WAYBEL_9:def 7;
   then reconsider k = j as Element of N|i;
      x = (N|i).k by A4,WAYBEL_9:16 .= (the mapping of N|i).j by WAYBEL_0:def 8
;
   hence thesis by A1,A5,FUNCT_1:def 5;
  end;

theorem Th9:
 for S being non empty 1-sorted, N being net of S
 for A being Subset of S,N holds N is_eventually_in A
  proof let S be non empty 1-sorted, N be net of S;
   let A be Subset of S,N;
   consider i being Element of N such that
A1: A = rng the mapping of N|i by Def2;
   take i; let j be Element of N; assume i <= j;
    then j in the carrier of N|i by WAYBEL_9:def 7;
   then reconsider j' = j as Element of N|i;
      N.j = (N|i).j' by WAYBEL_9:16 .= (the mapping of N|i).j' by WAYBEL_0:def
8
;
   hence thesis by A1,FUNCT_2:6;
  end;

theorem
   for S being non empty 1-sorted, N being net of S
 for F being finite non empty set st
    for A being Element of F holds A is Subset of S,N
 ex B being Subset of S,N st B c= meet F
  proof let S be non empty 1-sorted, N be net of S;
   let F be finite non empty set such that
A1: for A being Element of F holds A is Subset of S,N;
   defpred P[set,set] means
    ex i being Element of N st $2 = i & $1 = rng the mapping of N|i;
A2: now let x; assume x in F;
     then reconsider A = x as Subset of S, N by A1;
     consider i being Element of N such that
A3:   A = rng the mapping of N|i by Def2;
     reconsider y = i as set;
     take y; thus y in the carrier of N;
     thus P[x, y] by A3;
    end;
   consider f being Function such that
A4: dom f = F & rng f c= the carrier of N and
A5: for x st x in F holds P[x, f.x] from NonUniqBoundFuncEx(A2);
   reconsider B = rng f as finite Subset of N
     by A4,FINSET_1:26;
      [#]N is directed & [#]N = the carrier of N
     by PRE_TOPC:12,WAYBEL_0:def 6;
   then consider j being Element of N such that j in [#]N and
A6: j is_>=_than B by WAYBEL_0:1;
   reconsider C = rng the mapping of N|j as Subset of S, N by Th7;
   take C; let x; assume x in C;
   then consider y such that
A7: y in dom the mapping of N|j & x = (the mapping of N|j).y by FUNCT_1:def 5;
A8: y in the carrier of N|j by A7;
   reconsider y as Element of N|j by A7;
      the carrier of N|j = {k where k is Element of N: j <= k}
     by WAYBEL_9:12;
   then consider k being Element of N such that
A9: y = k & j <= k by A8;
      now let X; assume
A10:   X in F;
     then consider i being Element of N such that
A11:   f.X = i & X = rng the mapping of N|i by A5;
        i in B by A4,A10,A11,FUNCT_1:def 5;
      then i <= j by A6,LATTICE3:def 9;
      then i <= k by A9,ORDERS_1:26;
      then y in {l where l is Element of N: i <= l} by A9;
      then y in the carrier of N|i by WAYBEL_9:12;
     then reconsider z = y as Element of N|i;
        x = (N|j).y by A7,WAYBEL_0:def 8 .= N.k by A9,WAYBEL_9:16
       .= (N|i).z by A9,WAYBEL_9:16
       .= (the mapping of N|i).z by WAYBEL_0:def 8;
     hence x in X by A11,FUNCT_2:6;
    end;
   hence thesis by SETFAM_1:def 1;
 end;

definition
 let T be non empty 1-sorted;
 let N be non empty NetStr over T;
 func a_filter N -> Subset of BoolePoset [#]T equals:
Def3:
  {A where A is Subset of T: N is_eventually_in A};
 coherence
  proof
   set F = {A where A is Subset of T: N is_eventually_in A};
   set X = the carrier of T;
A1: BoolePoset X = InclPoset bool X by YELLOW_1:4
       .= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
A2: [#]T = X by PRE_TOPC:12;
      F c= bool X
     proof let x; assume x in F;
       then ex A being Subset of T st x = A & N is_eventually_in A;
      hence thesis;
     end;
   hence thesis by A1,A2;
  end;
end;

theorem Th11:
 for T being non empty 1-sorted
 for N being non empty NetStr over T
 for A being set
  holds A in a_filter N iff N is_eventually_in A & A is Subset of T
  proof let T be non empty 1-sorted;
   let N be non empty NetStr over T;
   let B be set;
      a_filter N = {A where A is Subset of T: N is_eventually_in A}
     by Def3;
    then B in a_filter N iff ex A being Subset of T st B = A & N
is_eventually_in A;
   hence thesis;
  end;

definition
 let T be non empty 1-sorted;
 let N be non empty NetStr over T;
 cluster a_filter N -> non empty upper;
 coherence
  proof set F = a_filter N;
   set X = the carrier of T, L = BoolePoset [#]T;
A1: BoolePoset X = InclPoset bool X by YELLOW_1:4
       .= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
A2: [#]T = X by PRE_TOPC:12;
      N is_eventually_in [#]T
     proof consider i being Element of N;
      take i; thus thesis by A2;
     end;
   hence F is non empty by Th11;
   let a,b be Element of L; assume a in F;
then A3: N is_eventually_in a by Th11;
   assume a <= b; then a c= b by YELLOW_1:2;
    then b is Subset of T & N is_eventually_in b
     by A1,A2,A3,WAYBEL_0:8;
   hence thesis by Th11;
  end;
end;

definition
 let T be non empty 1-sorted;
 let N be net of T;
 cluster a_filter N -> proper filtered;
 coherence
  proof set F = a_filter N;
   set X = the carrier of T, L = BoolePoset [#]T;
A1: BoolePoset X = InclPoset bool X by YELLOW_1:4
       .= RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
A2: [#]T = X by PRE_TOPC:12;
      now thus {} c= X by XBOOLE_1:2;
     assume {} in F;
      then N is_eventually_in {} by Th11;
     then consider i being Element of N such that
A3:   for j being Element of N st i <= j holds N.j in {} by WAYBEL_0:def 11;
     consider j being Element of N such that
A4:   i <= j & i <= j by YELLOW_6:def 5;
     thus contradiction by A3,A4;
    end;
    then F <> bool X;
   hence F is proper by A1,A2,TEX_2:5;
   let a,b be Element of L; assume a in F & b in F;
then A5: N is_eventually_in a & N is_eventually_in b by Th11;
   then consider i1 being Element of N such that
A6: for j being Element of N st i1 <= j holds N.j in a by WAYBEL_0:def 11;
   consider i2 being Element of N such that
A7: for j being Element of N st i2 <= j holds N.j in b
     by A5,WAYBEL_0:def 11;
   consider i being Element of N such that
A8: i1 <= i & i2 <= i by YELLOW_6:def 5;
   take z = a"/\"b;
A9: z = a/\b & z is Subset of T by A1,A2,YELLOW_1:17;
      now let j be Element of N; assume i <= j;
      then i1 <= j & i2 <= j by A8,ORDERS_1:26;
      then N.j in a & N.j in b by A6,A7;
     hence N.j in a/\b by XBOOLE_0:def 3;
    end;
    then N is_eventually_in z by A9,WAYBEL_0:def 11;
   hence z in F by A9,Th11;
      z c= a & z c= b by A9,XBOOLE_1:17;
   hence thesis by YELLOW_1:2;
  end;
end;

theorem Th12:
 for T being non empty TopSpace
 for N being net of T
 for x being Point of T holds
    x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N, T
  proof let T be non empty TopSpace;
   let N be net of T; set F = a_filter N;
   let x be Point of T;
   thus x is_a_cluster_point_of N implies x is_a_cluster_point_of F, T
     proof assume
A1:    for O being a_neighborhood of x holds N is_often_in O;
      let A be Subset of T; assume A is open & x in A;
       then A is a_neighborhood of x by CONNSP_2:5;
then A2:    N is_often_in A by A1;
      let B be set; assume B in F;
       then N is_eventually_in B by Th11;
      then consider i being Element of N such that
A3:    for j being Element of N st i <= j holds N.j in B by WAYBEL_0:def 11;
      consider j being Element of N such that
A4:    i <= j & N.j in A by A2,WAYBEL_0:def 12;
        now take a = N.j; thus a in B & a in A by A3,A4; end;
      hence thesis by XBOOLE_0:3;
     end;
   assume
A5: for A being Subset of T st A is open & x in A
     for B being set st B in F holds A meets B;
   let O be a_neighborhood of x;
   let i be Element of N;
   reconsider B = rng the mapping of N|i as Subset of T,N by Th7;
      N is_eventually_in B by Th9;
    then B in F & x in Int O by Th11,CONNSP_2:def 1;
    then Int O meets B by A5;
   then consider x being set such that
A6: x in Int O & x in B by XBOOLE_0:3;
   consider j being Element of N such that
A7: i <= j & x = N.j by A6,Th8;
   take j; Int O c= O by TOPS_1:44;
   hence thesis by A6,A7;
  end;

theorem Th13:
 for T being non empty TopSpace
 for N being net of T
 for x being Point of T holds
    x in Lim N iff x is_a_convergence_point_of a_filter N, T
  proof let T be non empty TopSpace;
   let N be net of T; set F = a_filter N;
   let x be Point of T;
   thus x in Lim N implies x is_a_convergence_point_of F, T
     proof assume
A1:    x in Lim N;
      let A be Subset of T; assume A is open & x in A;
       then A is a_neighborhood of x by CONNSP_2:5;
       then N is_eventually_in A by A1,YELLOW_6:def 18;
      hence thesis by Th11;
     end;
   assume
A2: for A being Subset of T st A is open & x in A holds A in F;
      now let O be a_neighborhood of x;
        x in Int O by CONNSP_2:def 1;
      then Int O in F by A2;
      then Int O c= O & N is_eventually_in Int O by Th11,TOPS_1:44;
     hence N is_eventually_in O by WAYBEL_0:8;
    end;
   hence thesis by YELLOW_6:def 18;
  end;

definition
 let L be non empty 1-sorted;
 let O be non empty Subset of L;
 let F be Filter of BoolePoset O;
 func a_net F -> strict non empty NetStr over L means:
Def4:
  the carrier of it
     = {[a, f] where a is Element of L, f is Element of F: a in f} &
  (for i,j being Element of it holds i <= j iff j`2 c= i`2) &
  for i being Element of it holds it.i = i`1;
 existence
 proof
   set S = {[a, f] where a is Element of L, f is Element of F: a in f};
     Top BoolePoset O = O by YELLOW_1:19;
   then reconsider f = O as Element of F by WAYBEL12:12;
   reconsider f as Subset of L;
   consider a being Element of L such that
A1:a in f by SUBSET_1:10;
   reconsider a as Element of L;
     [a, f] in S by A1;
   then reconsider S as non empty set;
   defpred P[set,set] means $2`2 c= $1`2;
   consider R being Relation of S,S such that
A2:for x,y being Element of S holds
   [x,y] in R iff P[x,y] from Rel_On_Dom_Ex;
   deffunc F(set) = $1`1;
A3:for x being set st x in S holds F(x) in the carrier of L
   proof
    let x be set;
    assume x in S;
    then consider a being Element of L, f being Element of F such that
A4: x = [a, f] & a in f;
      x`1 = a by A4,MCART_1:def 1;
    hence thesis;
   end;
   consider h being Function of S, the carrier of L such that
A5:for x being set st x in S holds h.x = F(x) from Lambda1(A3);
   take N=NetStr(#S,R,h#);
A6:for i,j being Element of N holds i <= j iff j`2 c= i`2
   proof
    let i,j be Element of N;
    reconsider x = i, y = j as Element of S;
      [x,y] in the InternalRel of N iff y`2 c= x`2 by A2;
    hence thesis by ORDERS_1:def 9;
   end;
     for i being Element of N holds N.i = i`1
   proof
    let i being Element of N;
    reconsider x = i as Element of S;
      h.x = N.i by WAYBEL_0:def 8;
    hence thesis by A5;
   end;
   hence thesis by A6;
 end;
 uniqueness
 proof
   let it1,it2 be strict non empty NetStr over L such that
A7:the carrier of it1
     = {[a, f] where a is Element of L, f is Element of F: a in f} and
A8:(for i,j being Element of it1 holds i <= j iff j`2 c= i`2) and
A9:for i being Element of it1 holds it1.i = i`1 and
A10:the carrier of it2
     = {[a, f] where a is Element of L, f is Element of F: a in f} and
A11:(for i,j being Element of it2 holds i <= j iff j`2 c= i`2) and
A12:for i being Element of it2 holds it2.i = i`1;
   set S = {[a, f] where a is Element of L, f is Element of F: a in f};
A13:the InternalRel of it1 = the InternalRel of it2
   proof
      for x,y being set holds [x,y] in the InternalRel of it1 iff
    [x,y] in the InternalRel of it2
    proof
     let x,y be set;
     hereby assume
A14:   [x,y] in the InternalRel of it1;
then A15:   x in S & y in S by A7,ZFMISC_1:106;
      then reconsider i=x, j=y as Element of it1 by A7;
      reconsider i'=x, j'=y as Element of it2 by A10,A15;
        i <= j by A14,ORDERS_1:def 9;
      then (j')`2 c= (i')`2 by A8;
      then i' <= j' by A11;
      hence [x,y] in the InternalRel of it2 by ORDERS_1:def 9;
     end;
     assume A16:[x,y] in the InternalRel of it2;
then A17: x in S & y in S by A10,ZFMISC_1:106;
     then reconsider i=x, j=y as Element of it2 by A10;
     reconsider i'=x, j'=y as Element of it1 by A7,A17;
       i <= j by A16,ORDERS_1:def 9;
     then (j')`2 c= (i')`2 by A11;
     then i' <= j' by A8;
     hence [x,y] in the InternalRel of it1 by ORDERS_1:def 9;
     end;
    hence thesis by RELAT_1:def 2;
   end;
     the mapping of it1 = the mapping of it2
   proof
    reconsider f1 =the mapping of it1 as Function of S, the carrier of L by A7;
    reconsider f2 =the mapping of it2 as Function of S, the carrier of L by A10
;

      for x being set st x in S holds f1.x = f2.x
    proof
     let x be set;
     assume A18:x in S;
     then reconsider x1 = x as Element of it1 by A7;
     reconsider x2 = x as Element of it2 by A10,A18;
     reconsider x as Element of S by A18;
       f1.x = it1.x1 by WAYBEL_0:def 8 .=x1`1 by A9 .= it2.x2 by A12;
     hence thesis by WAYBEL_0:def 8;
    end;
    hence thesis by FUNCT_2:18;
   end;
   hence thesis by A7,A10,A13;
 end;
end;

definition
 let L be non empty 1-sorted;
 let O be non empty Subset of L;
 let F be Filter of BoolePoset O;
 cluster a_net F -> reflexive transitive;
 coherence
 proof
     for x,y,z being set st x in the carrier of a_net F &
   y in the carrier of a_net F & z in the carrier of a_net F &
   [x,y] in the InternalRel of a_net F & [y,z] in the InternalRel of a_net F
   holds [x,z] in the InternalRel of a_net F
   proof
    let x,y,z be set;
    assume that A1:x in the carrier of a_net F and
A2: y in the carrier of a_net F and
A3: z in the carrier of a_net F and
A4: [x,y] in the InternalRel of a_net F and
A5: [y,z] in the InternalRel of a_net F;
    reconsider i=x as Element of a_net F by A1;
    reconsider j=y as Element of a_net F by A2;
    reconsider k=z as Element of a_net F by A3;
      i <= j & j <= k by A4,A5,ORDERS_1:def 9;
    then j`2 c= i`2 & k`2 c= j`2 by Def4;
    then k`2 c= i`2 by XBOOLE_1:1;
    then i <= k by Def4;
    hence thesis by ORDERS_1:def 9;
   end;
then A6:the InternalRel of (a_net F) is_transitive_in the carrier of (a_net F)
   by RELAT_2:def 8;
     for x being set st x in the carrier of a_net F holds
   [x,x] in the InternalRel of a_net F
   proof
    let x being set;
    assume x in the carrier of a_net F;
    then reconsider i=x as Element of a_net F;
      i`2 c= i`2;
    then i <= i by Def4;
    hence thesis by ORDERS_1:def 9;
   end;
   then the InternalRel of (a_net F) is_reflexive_in the carrier of (a_net F)
   by RELAT_2:def 1;
   hence thesis by A6,ORDERS_1:def 4,def 5;
 end;
end;

definition
 let L be non empty 1-sorted;
 let O be non empty Subset of L;
 let F be proper Filter of BoolePoset O;
 cluster a_net F -> directed;
 coherence
 proof
   set S = {[a, f] where a is Element of L, f is Element of F: a in f};
     for x,y being Element of a_net F st x in [#](a_net F) & y in [#](a_net F)
    ex z being Element of a_net F st z in [#](a_net F) & x <= z & y <= z
   proof
    let x,y being Element of a_net F;
    assume x in [#](a_net F) & y in [#](a_net F);
      x in the carrier of a_net F & y in the carrier of a_net F;
then A1: x in S & y in S by Def4;
    then consider a being Element of L, f being Element of F such that
A2: x = [a, f] & a in f;
    consider b being Element of L, g being Element of F such that
A3: y = [b, g] & b in g by A1;
    reconsider f as Element of BoolePoset O;
    reconsider g as Element of BoolePoset O;
    reconsider h = f "/\" g as Element of F by WAYBEL_0:41;
    consider s being Element of h;
      not Bottom (BoolePoset O) in F by WAYBEL_7:8;
    then not {} in F by YELLOW_1:18;
then A4:  h <> {};
then A5: s in h;
      h c= O by WAYBEL_8:28;
    then s in O by A5;
    then reconsider s as Element of L;
      [s,h] in S by A4;
then A6: [s,h] in the carrier of a_net F by Def4;
    then reconsider z = [s,h] as Element of a_net F;
    reconsider i = x, j = y, k = z as Element of a_net F;
A7: i`2 = f & j`2 = g & k`2 = h by A2,A3,MCART_1:def 2;
      h c= f /\ g & f /\ g c= f & f /\ g c= g by XBOOLE_1:17,YELLOW_1:17;
    then A8: h c= f & h c= g by XBOOLE_1:1;
    take z;
    thus thesis by A6,A7,A8,Def4,PRE_TOPC:12;
   end;
   then [#](a_net F) is directed by WAYBEL_0:def 1;
  hence a_net F is directed by WAYBEL_0:def 6;
 end;
end;

theorem Th14:
 for T being non empty 1-sorted
 for F being Filter of BoolePoset [#]T
  holds F \ {{}} = a_filter a_net F
  proof let T be non empty 1-sorted;
   let F be Filter of BoolePoset [#]T;
      BoolePoset [#]T = InclPoset bool [#]T by YELLOW_1:4;
then A1: the carrier of BoolePoset [#]T = bool [#]T by YELLOW_1:1;
A2: [#]T = the carrier of T by PRE_TOPC:12;
   set X = a_filter a_net F;
A3: the carrier of a_net F
     = {[a, f] where a is Element of T, f is Element of F: a in f} by Def4;
   thus F \ {{}} c= X
     proof let x; assume
         x in F \ {{}};
then A4:    x in F & not x in {{}} by XBOOLE_0:def 4;
      then reconsider A = x as Subset of T by A1,A2;
      consider a being Element of A;
A5:    A <> {} by A4,TARSKI:def 1; then a in A;
      then reconsider a as Element of T;
         [a, A] in the carrier of a_net F by A3,A4,A5;
      then reconsider i = [a, A] as Element of a_net F;
         a_net F is_eventually_in A
        proof take i; let j be Element of a_net F;
            j in the carrier of a_net F;
         then consider a being Element of T, f being Element of F such that
A6:       j = [a,f] & a in f by A3;
         assume i <= j;
then A7:       j`2 c= i`2 & (a_net F).j = j`1 by Def4;
            j`2 = f & i`2 = A & j`1 = a by A6,MCART_1:7;
         hence thesis by A6,A7;
        end;
      hence thesis by Th11;
     end;
   let x; assume x in X;
then A8: a_net F is_eventually_in x & x is Subset of T by Th11;
   then consider i being Element of a_net F such that
A9: for j being Element of a_net F st i <= j holds (a_net F).j in x
     by WAYBEL_0:def 11;
      i in the carrier of a_net F;
   then consider a being Element of T, f being Element of F such that
A10: i = [a,f] & a in f by A3;
    A11: f c= x
     proof let x; assume
A12:    x in f;
      then reconsider b = x as Element of T by A1,A2;
         [b,f] in the carrier of a_net F by A3,A12;
      then reconsider j = [b,f] as Element of a_net F;
         j`2 = f & i`2 = f & j`1 = b by A10,MCART_1:7;
       then i <= j & (a_net F).j = b by Def4;
      hence thesis by A9;
     end;
then A13: x in F & a in x by A2,A8,A10,WAYBEL_7:11;
      not x in {{}} by A10,A11,TARSKI:def 1;
   hence thesis by A13,XBOOLE_0:def 4;
  end;

theorem Th15:
 for T being non empty 1-sorted
 for F being proper Filter of BoolePoset [#]T
  holds F = a_filter a_net F
  proof let T be non empty 1-sorted;
   let F be proper Filter of BoolePoset [#]T;
      not {} in F by Th2;
    then F \ {{}} = F by ZFMISC_1:65;
   hence thesis by Th14;
  end;

theorem Th16:
 for T being non empty 1-sorted
 for F being Filter of BoolePoset [#]T
 for A being non empty Subset of T holds
   A in F iff a_net F is_eventually_in A
  proof let T be non empty 1-sorted;
   let F be Filter of BoolePoset [#]T;
A1: F\{{}} = a_filter a_net F by Th14;
   let B be non empty Subset of T;
      B in F iff B in F\{{}} by ZFMISC_1:64;
   hence thesis by A1,Th11;
  end;

theorem Th17:
 for T being non empty TopSpace
 for F being proper Filter of BoolePoset [#]T
 for x being Point of T holds
    x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F, T
  proof let T be non empty TopSpace;
   let F be proper Filter of BoolePoset [#]T;
      F = a_filter a_net F by Th15;
   hence thesis by Th12;
  end;

theorem Th18:
 for T being non empty TopSpace
 for F being proper Filter of BoolePoset [#]T
 for x being Point of T holds
    x in Lim a_net F iff x is_a_convergence_point_of F, T
  proof let T be non empty TopSpace;
   let F be proper Filter of BoolePoset [#]T;
      F = a_filter a_net F by Th15;
   hence thesis by Th13;
  end;

canceled;

theorem Th20:
 for T being non empty TopSpace, x being Point of T, A being Subset of T
  st x in Cl A
 for F being proper Filter of BoolePoset [#]T st F = NeighborhoodSystem x
  holds a_net F is_often_in A
  proof let T be non empty TopSpace, x be Point of T, A be Subset of T; assume
A1: x in Cl A;
   let F be proper Filter of BoolePoset [#]T such that
A2: F = NeighborhoodSystem x;
   set N = a_net F;
A3: the carrier of N
     = {[a, f] where a is Element of T, f is Element of F: a in f} by Def4;
   let i be Element of N; i in the carrier of N;
   then consider a being Element of T, f being Element of F such that
A4: i = [a, f] & a in f by A3;
   reconsider f as a_neighborhood of x by A2,Th3;
      f meets A by A1,YELLOW_6:6;
   then consider b being set such that
A5: b in f & b in A by XBOOLE_0:3;
   reconsider b as Element of T by A5;
      [b, f] in the carrier of N by A3,A5;
   then reconsider j = [b, f] as Element of N;
   take j;
      i`2 = f & j`2 = f & j`1 = b by A4,MCART_1:7;
   hence i <= j & N.j in A by A5,Def4;
  end;

theorem Th21:
 for T being non empty 1-sorted, A being set
 for N being net of T st N is_eventually_in A
 for S being subnet of N
  holds S is_eventually_in A
  proof let T be non empty 1-sorted, A be set;
   let N be net of T; given i being Element of N such that
A1: for j being Element of N st i <= j holds N.j in A;
   let S be subnet of N;
   consider f being map of S, N such that
A2: the mapping of S = (the mapping of N)*f and
A3: for m being Element of N ex n being Element of S st
    for p being Element of S st n <= p holds m <= f.p by YELLOW_6:def 12;
   consider n being Element of S such that
A4: for p being Element of S st n <= p holds i <= f.p by A3;
   take n; let p be Element of S; assume n <= p;
    then i <= f.p by A4;
then A5: N.(f.p) in A by A1;
      S.p = (the mapping of S).p by WAYBEL_0:def 8
       .= (the mapping of N).(f.p) by A2,FUNCT_2:21;
   hence thesis by A5,WAYBEL_0:def 8;
  end;

theorem Th22:
 for T being non empty TopSpace, F,G,x being set
  st F c= G & x is_a_convergence_point_of F, T
  holds x is_a_convergence_point_of G, T
  proof let T be non empty TopSpace, F,G,x be set such that
A1: F c= G and
A2: for A being Subset of T st A is open & x in A holds A in F;
   let A be Subset of T; assume A is open & x in A;
    then A in F by A2;
   hence thesis by A1;
  end;

theorem Th23:
 for T being non empty TopSpace, A being Subset of T
 for x being Point of T holds
   x in Cl A
  iff
   ex N being net of T st N is_eventually_in A & x is_a_cluster_point_of N
  proof let T be non empty TopSpace, A be Subset of T;
   let x be Point of T;
   reconsider F = NeighborhoodSystem x as proper Filter of BoolePoset [#]T;
   hereby assume x in Cl A;
      then a_net F is_often_in A by Th20;
     then reconsider N = (a_net F)"A as subnet of a_net F by YELLOW_6:31;
     reconsider N' = N as net of T;
     take N'; thus N' is_eventually_in A by YELLOW_6:32;
        x is_a_convergence_point_of F, T by Th4;
      then x in Lim a_net F & Lim a_net F c= Lim N by Th18,YELLOW_6:41;
     hence x is_a_cluster_point_of N' by WAYBEL_9:29;
    end;
   given N being net of T such that
A1: N is_eventually_in A & x is_a_cluster_point_of N;
   consider i being Element of N such that
A2: for j being Element of N st i <= j holds N.j in A by A1,WAYBEL_0:def 11;
      now let G be Subset of T; assume
A3:   G is open & x in G;
      then Int G = G by TOPS_1:55;
      then G is a_neighborhood of x by A3,CONNSP_2:def 1;
      then N is_often_in G by A1,WAYBEL_9:def 9;
     then consider j being Element of N such that
A4:   i <= j & N.j in G by WAYBEL_0:def 12;
        N.j in A by A2,A4;
     hence A meets G by A4,XBOOLE_0:3;
    end;
   hence thesis by PRE_TOPC:def 13;
  end;

theorem Th24:
 for T being non empty TopSpace, A being Subset of T
 for x being Point of T holds
   x in Cl A
  iff
   ex N being convergent net of T st N is_eventually_in A & x in Lim N
  proof let T be non empty TopSpace, A be Subset of T;
   let x be Point of T;
   hereby assume x in Cl A;
     then consider N being net of T such that
A1:   N is_eventually_in A & x is_a_cluster_point_of N by Th23;
     consider S being subnet of N such that
A2:   x in Lim S by A1,WAYBEL_9:32;
     reconsider S as convergent net of T by A2,YELLOW_6:def 19;
     take S; thus S is_eventually_in A by A1,Th21;
     thus x in Lim S by A2;
    end;
   given N being convergent net of T such that
A3: N is_eventually_in A & x in Lim N;
      x is_a_cluster_point_of N by A3,WAYBEL_9:29;
   hence thesis by A3,Th23;
  end;

theorem
   for T being non empty TopSpace, A being Subset of T holds
   A is closed
  iff
   for N being net of T st N is_eventually_in A
   for x being Point of T st x is_a_cluster_point_of N
    holds x in A
  proof let T be non empty TopSpace, A be Subset of T;
     A is closed iff Cl A = A by PRE_TOPC:52;
   hence A is closed implies
     for N being net of T st N is_eventually_in A
      for x being Point of T st x is_a_cluster_point_of N
       holds x in A by Th23;
   assume
A1: for N being net of T st N is_eventually_in A
    for x being Point of T st x is_a_cluster_point_of N
     holds x in A;
      A = Cl A
     proof thus A c= Cl A by PRE_TOPC:48;
      let x; assume
A2:    x in Cl A; then reconsider y = x as Element of T;
         ex N being net of T st N is_eventually_in A & y is_a_cluster_point_of
N
        by A2,Th23;
      hence thesis by A1;
     end;
   hence thesis;
  end;

theorem
   for T being non empty TopSpace, A being Subset of T holds
   A is closed
  iff
   for N being convergent net of T st N is_eventually_in A
   for x being Point of T st x in Lim N
    holds x in A
  proof let T be non empty TopSpace, A be Subset of T;
     A is closed iff Cl A = A by PRE_TOPC:52;
   hence A is closed implies
     for N being convergent net of T st N is_eventually_in A
      for x being Point of T st x in Lim N
       holds x in A by Th24;
   assume
A1: for N being convergent net of T st N is_eventually_in A
    for x being Point of T st x in Lim N holds x in A;
      A = Cl A
     proof thus A c= Cl A by PRE_TOPC:48;
      let x; assume
A2:    x in Cl A; then reconsider y = x as Element of T;
         ex N being convergent net of T
        st N is_eventually_in A & y in Lim N by A2,Th24;
      hence thesis by A1;
     end;
   hence thesis;
  end;

theorem Th27:
 for T being non empty TopSpace, A being Subset of T
 for x being Point of T holds
   x in Cl A
  iff
   ex F being proper Filter of BoolePoset [#]T
    st A in F & x is_a_cluster_point_of F, T
  proof let T be non empty TopSpace, A be Subset of T;
   let x be Point of T;
   hereby assume x in Cl A;
     then consider N being net of T such that
A1:   N is_eventually_in A & x is_a_cluster_point_of N by Th23;
     set F = a_filter N;
     take F; thus A in F by A1,Th11;
     thus x is_a_cluster_point_of F, T by A1,Th12;
    end;
   given F being proper Filter of BoolePoset [#]T such that
A2: A in F & x is_a_cluster_point_of F, T;
   reconsider F' = F as proper Filter of BoolePoset [#]T;
      a_filter a_net F' = F by Th15;
    then a_net F' is_eventually_in A & x is_a_cluster_point_of a_net F'
     by A2,Th11,Th12;
   hence thesis by Th23;
  end;

theorem Th28:
 for T being non empty TopSpace, A being Subset of T
 for x being Point of T holds
   x in Cl A
  iff
   ex F being ultra Filter of BoolePoset [#]T
    st A in F & x is_a_convergence_point_of F, T
  proof let T be non empty TopSpace, A be Subset of T;
   let x be Point of T;
   set X = the carrier of T;
A1: [#]T = X by PRE_TOPC:12;
   hereby assume x in Cl A;
     then consider N being net of T such that
A2:   N is_eventually_in A & x is_a_cluster_point_of N by Th23;
     consider S being subnet of N such that
A3:   x in Lim S by A2,WAYBEL_9:32;
     set F = a_filter S;
     consider G being Filter of BoolePoset [#]T such that
A4:   F c= G & G is ultra by WAYBEL_7:30;
     reconsider G as ultra Filter of BoolePoset [#]T by A4;
     take G;
        S is_eventually_in A by A2,Th21;
      then A in F by Th11;
     hence A in G by A4;
        x is_a_convergence_point_of F, T by A3,Th13;
     hence x is_a_convergence_point_of G, T by A4,Th22;
    end;
   given F being ultra Filter of BoolePoset [#]T such that
A5: A in F & x is_a_convergence_point_of F, T;
      x is_a_cluster_point_of F, T by A1,A5,WAYBEL_7:31;
   hence thesis by A5,Th27;
  end;

theorem
   for T being non empty TopSpace, A being Subset of T holds
   A is closed
  iff
   for F being proper Filter of BoolePoset [#]T st A in F
   for x being Point of T st x is_a_cluster_point_of F,T
    holds x in A
  proof let T be non empty TopSpace, A be Subset of T;
     A is closed iff Cl A = A by PRE_TOPC:52;
   hence A is closed implies
     for F being proper Filter of BoolePoset [#]T st A in F
      for x being Point of T st x is_a_cluster_point_of F,T
       holds x in A by Th27;
   assume
A1: for F being proper Filter of BoolePoset [#]T st A in F
    for x being Point of T st x is_a_cluster_point_of F,T
     holds x in A;
      A = Cl A
     proof thus A c= Cl A by PRE_TOPC:48;
      let x; assume
A2:    x in Cl A; then reconsider y = x as Element of T;
         ex F being proper Filter of BoolePoset [#]T
        st A in F & y is_a_cluster_point_of F, T by A2,Th27;
      hence thesis by A1;
     end;
   hence thesis;
  end;

theorem
   for T being non empty TopSpace, A being Subset of T holds
   A is closed
  iff
   for F being ultra Filter of BoolePoset [#]T st A in F
   for x being Point of T st x is_a_convergence_point_of F,T
    holds x in A
  proof let T be non empty TopSpace, A be Subset of T;
     A is closed iff Cl A = A by PRE_TOPC:52;
   hence A is closed implies
     for F being ultra Filter of BoolePoset [#]T st A in F
      for x being Point of T st x is_a_convergence_point_of F,T
       holds x in A by Th28;
   assume
A1: for F being ultra Filter of BoolePoset [#]T st A in F
    for x being Point of T st x is_a_convergence_point_of F,T
     holds x in A;
      A = Cl A
     proof thus A c= Cl A by PRE_TOPC:48;
      let x; assume
A2:    x in Cl A; then reconsider y = x as Element of T;
         ex F being ultra Filter of BoolePoset [#]T
        st A in F & y is_a_convergence_point_of F, T by A2,Th28;
      hence thesis by A1;
     end;
   hence thesis;
  end;

theorem Th31:
 for T being non empty TopSpace, N being net of T
 for s being Point of T holds
   s is_a_cluster_point_of N iff
    for A being Subset of T,N holds s in Cl A
  proof let T be non empty TopSpace, N be net of T;
   let s be Point of T;
   hereby assume
A1:   s is_a_cluster_point_of N;
     let A be Subset of T,N;
        N is_eventually_in A by Th9;
     hence s in Cl A by A1,Th23;
    end;
   assume
A2: for A being Subset of T,N holds s in Cl A;
   let V be a_neighborhood of s;
   let i be Element of N;
   reconsider A = rng the mapping of N|i as Subset of T,N by Th7;
   consider x being Element of A /\ Int V;
      s in Int V & Int V is open & s in Cl A by A2,CONNSP_2:def 1;
    then A meets Int V by PRE_TOPC:def 13;
    then A /\ Int V <> {}T by XBOOLE_0:def 7;
then A3: x in A & x in Int V by XBOOLE_0:def 3;
   then consider j being set such that
A4: j in dom the mapping of N|i & x = (the mapping of N|i).j
     by FUNCT_1:def 5;
A5: dom the mapping of N|i = the carrier of N|i by FUNCT_2:def 1;
   reconsider j as Element of N|i by A4;
      the carrier of N|i = {l where l is Element of N: i <= l}
     by WAYBEL_9:12;
   then consider l being Element of N such that
A6: j = l & i <= l by A4,A5;
   take l; thus i <= l by A6;
A7: x = (N|i).j by A4,WAYBEL_0:def 8 .= N.l by A6,WAYBEL_9:16;
      Int V c= V by TOPS_1:44;
   hence N.l in V by A3,A7;
  end;

theorem
  for T being non empty TopSpace
 for F being Subset-Family of T st F is closed
  holds FinMeetCl F is closed
  proof let T be non empty TopSpace;
   let F be Subset-Family of T such that
A1: F is closed;
      now let P be Subset of T; assume P in FinMeetCl F;
     then consider Y being Subset-Family of T such that
A2:   Y c= F & Y is finite & P = Intersect Y by CANTOR_1:def 4;
A3:   for A being Subset of T st A in Y holds A is closed
       by A1,A2,TOPS_2:def 2;
        Y = {} or Y <> {};
      then P = the carrier of T & the carrier of T = [#]T or
      P = meet Y by A2,CANTOR_1:def 3,PRE_TOPC:12;
     hence P is closed by A3,PRE_TOPC:44;
    end;
   hence thesis by TOPS_2:def 2;
  end;

Lm1:
 for T being non empty TopSpace st T is compact
  for N being net of T ex x being Point of T st
    x is_a_cluster_point_of N
  proof let T be non empty TopSpace such that
A1: T is compact;
   let N be net of T;
   set F = {Cl A where A is Subset of T, N: not contradiction};
      F c= bool the carrier of T
     proof let x; assume x in F;
       then ex A being Subset of T, N st x = Cl A;
      hence thesis;
     end;
    then F is Subset-Family of T by SETFAM_1:def 7;
   then reconsider F as Subset-Family of T;
   consider x being Element of meet F;
A2: F is closed
     proof let S be Subset of T; assume S in F;
       then ex A being Subset of T,N st S = Cl A;
      hence S is closed;
     end;
      F is centered
     proof consider A0 being Subset of T, N;
         Cl A0 in F;
      hence F <> {};
      let G be set such that
A3:    G <> {} & G c= F & G is finite;
      defpred P[set,set] means
       ex A being Subset of T,N, i being Element of N st
        $1 = Cl A & $2 = i & A = rng the mapping of N|i;
A4:    now let x; assume x in G;
         then x in F by A3;
        then consider A being Subset of T, N such that
A5:      x = Cl A;
        consider i being Element of N such that
A6:      A = rng the mapping of N|i by Def2;
        reconsider y = i as set;
        take y; thus y in the carrier of N;
        thus P[x, y] by A5,A6;
       end;
      consider f being Function such that
A7:    dom f = G & rng f c= the carrier of N and
A8:    for x st x in G holds P[x, f.x]  from NonUniqBoundFuncEx(A4);
      reconsider B = rng f as finite Subset of N
        by A3,A7,FINSET_1:26;
         [#]N is directed & [#]N = the carrier of N
        by PRE_TOPC:12,WAYBEL_0:def 6;
      then consider j being Element of N such that j in [#]N and
A9:    j is_>=_than B by WAYBEL_0:1;
         now let X; assume
A10:      X in G;
        then consider A being Subset of T,N, i being Element of N such that
A11:      X = Cl A & f.X = i & A = rng the mapping of N|i by A8;
           i in B by A7,A10,A11,FUNCT_1:def 5;
         then i <= j by A9,LATTICE3:def 9;
         then j in the carrier of N|i by WAYBEL_9:def 7;
         then j in dom the mapping of N|i &
         the mapping of N|i = (the mapping of N)|the carrier of (N|i)
          by FUNCT_2:def 1,WAYBEL_9:def 7;
         then (the mapping of N|i).j in A &
         (the mapping of N|i).j = (the mapping of N).j
          by A11,FUNCT_1:70,def 5;
         then N.j in A & A c= X by A11,PRE_TOPC:48,WAYBEL_0:def 8;
        hence N.j in X;
       end;
      hence meet G <> {} by A3,SETFAM_1:def 1;
     end;
then A12: meet F <> {} by A1,A2,COMPTS_1:13;
   then x in meet F;
   then reconsider x as Point of T;
   take x;
      now let A be Subset of T,N;
        Cl A in F;
     hence x in Cl A by A12,SETFAM_1:def 1;
    end;
   hence x is_a_cluster_point_of N by Th31;
  end;

Lm2:
 for T being non empty TopSpace st
    for N being net of T st N in NetUniv T
     ex x being Point of T st x is_a_cluster_point_of N
  holds T is compact
  proof let T be non empty TopSpace; assume
A1: for N being net of T st N in NetUniv T
     ex x being Point of T st x is_a_cluster_point_of N;
      now let F be Subset-Family of T such that
A2:   F is centered & F is closed;
     set G = FinMeetCl F;
     defpred P[set,set] means $2 in $1;
A3:   now let x; assume x in G;
       then consider Y being Subset-Family of T such that
A4:     Y c= F & Y is finite & x = Intersect Y by CANTOR_1:def 4;
       consider y being Element of x;
          Y = {} or Y <> {};
        then x = the carrier of T or x = meet Y & meet Y <> {}
         by A2,A4,CANTOR_1:def 3,COMPTS_1:def 2;
        then y in x;
       hence ex y st y in the carrier of T & P[x, y] by A4;
      end;
     consider f being Function such that
A5:   dom f = G & rng f c= the carrier of T and
A6:   for a being set st a in G holds P[a, f.a] from NonUniqBoundFuncEx(A3);
A7:   F <> {} & F c= G by A2,CANTOR_1:4,COMPTS_1:def 2;
     then reconsider G as non empty Subset-Family of T by XBOOLE_1:3;
     set R = (InclPoset G) opp;
      A8: InclPoset G = RelStr(#G, RelIncl G#) by YELLOW_1:def 1;
then A9:   the carrier of R = G by YELLOW_6:12;
        R is directed
       proof let x,y be Element of R such that x in [#]R & y in [#]R;
           x in G by A9;
        then consider X being Subset-Family of T such that
A10:      X c= F & X is finite & x = Intersect X by CANTOR_1:def 4;
           y in G by A9;
        then consider Y being Subset-Family of T such that
A11:      Y c= F & Y is finite & y = Intersect Y by CANTOR_1:def 4;
        set z = Intersect (X \/ Y);
           X \/ Y c= F & X \/ Y is finite by A10,A11,FINSET_1:14,XBOOLE_1:8;
         then z in G by CANTOR_1:def 4;
        then reconsider z as Element of R by A9;
        take z; z in the carrier of R;
        hence z in [#]R by PRE_TOPC:12;
           X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7;
         then z c= x & z c= y & ~x = x & ~y = y & ~z = z
          by A10,A11,CANTOR_1:11,LATTICE3:def 7;
         then ~z <= ~x & ~z <= ~y by YELLOW_1:3;
        hence x <= z & y <= z by YELLOW_7:1;
       end;
     then reconsider R as directed non empty transitive RelStr;
     reconsider f as Function of the carrier of R, the carrier of T
       by A5,A9,FUNCT_2:4;
     set N = R *' f;
A12:   the RelStr of N = the RelStr of R & the mapping of N = f
       by WAYBEL32:def 3;
     set X = the carrier of T;
A13:   the_universe_of X = Tarski-Class the_transitive-closure_of X
       by YELLOW_6:def 3;
        X c= the_transitive-closure_of X &
      the_transitive-closure_of X in Tarski-Class the_transitive-closure_of X
       by CLASSES1:5,59;
      then X in Tarski-Class the_transitive-closure_of X by CLASSES1:6;
      then bool X in Tarski-Class the_transitive-closure_of X by CLASSES1:7;
      then G in Tarski-Class the_transitive-closure_of X by CLASSES1:6;
      then N in NetUniv T by A9,A12,A13,YELLOW_6:def 14;
     then consider x being Point of T such that
A14:   x is_a_cluster_point_of N by A1;
        now let X; assume A15: X in F;
       then reconsider a = X as Element of N by A7,A9,A12;
       reconsider A = X as Subset of T by A15;
          A is closed by A2,A15,TOPS_2:def 2;
then A16:     Cl A = A by PRE_TOPC:52;
          now let V be Subset of T; assume
A17:       V is open & x in V;
          then Int V = V by TOPS_1:55;
          then V is a_neighborhood of x by A17,CONNSP_2:def 1;
          then N is_often_in V by A14,WAYBEL_9:def 9;
         then consider b being Element of N such that
A18:       a <= b & N.b in V by WAYBEL_0:def 12;
         reconsider a' = a, b' = b as Element of (InclPoset G) opp
           by A12;
A19:       N.b = f.b by A12,WAYBEL_0:def 8;
            a' <= b' by A12,A18,YELLOW_0:1;
          then ~a' >= ~b' & ~a' = A & ~b' = b by LATTICE3:def 7,YELLOW_7:1;
          then b c= A & N.b in b by A6,A8,A19,YELLOW_1:3;
         hence A meets V by A18,XBOOLE_0:3;
        end;
       hence x in X by A16,PRE_TOPC:def 13;
      end;
     hence meet F <> {} by A7,SETFAM_1:def 1;
    end;
   hence thesis by COMPTS_1:13;
  end;

theorem Th33:
 for T being non empty TopSpace holds
    T is compact
  iff
    for F being ultra Filter of BoolePoset [#]T
     ex x being Point of T st x is_a_convergence_point_of F, T
  proof let T be non empty TopSpace;
   set X = the carrier of T;
A1: the carrier of BoolePoset X = bool X by WAYBEL_7:4;
A2: [#]T = X by PRE_TOPC:12;
   hereby assume
A3:   T is compact;
     let F be ultra Filter of BoolePoset [#]T;
     set G = {Cl A where A is Subset of T: A in F};
        G c= bool the carrier of T
       proof let x; assume x in G;
         then ex A being Subset of T st x = Cl A & A in F;
        hence thesis;
       end;
      then G is Subset-Family of T by SETFAM_1:def 7;
     then reconsider G as Subset-Family of T;
A4:   G is centered
       proof consider A0 being Element of F;
        reconsider A0 as Subset of T by A1,A2; Cl A0 in G;
        hence G <> {};
        let H be set; assume
A5:      H <> {} & H c= G & H is finite;
         then H c= bool X by XBOOLE_1:1;
        then reconsider H1 = H as finite Subset-Family of X by A5,SETFAM_1:def
7;
           H1 c= F
          proof let x; assume x in H1;
            then x in G by A5;
           then consider A being Subset of T such that
A6:         x = Cl A & A in F;
              A c= Cl A by PRE_TOPC:48;
           hence thesis by A2,A6,WAYBEL_7:11;
          end;
         then Intersect H1 in F by A2,WAYBEL_7:15;
         then Intersect H1 <> {} by Th2;
        hence meet H <> {} by A5,CANTOR_1:def 3;
       end;
     consider x being Element of meet G;
        G is closed
       proof let A be Subset of T; assume A in G;
         then ex B being Subset of T st A = Cl B & B in F;
        hence thesis;
       end;
      then A7: meet G <> {} by A3,A4,COMPTS_1:13;
then x in meet G;
     then reconsider x as Point of T;
     take x;
     thus x is_a_convergence_point_of F, T
       proof let A be Subset of T such that
A8:      A is open & x in A;
         A9: F is prime by WAYBEL_7:26;
        set B = A`;
           [#]T = X by PRE_TOPC:12;
then A10:      B = X\A by PRE_TOPC:17;
           now assume B in F;
           then Cl B in G & B is closed by A8,TOPS_1:30;
           then B in G & not x in B by A8,A10,PRE_TOPC:52,XBOOLE_0:def 4;
          hence contradiction by A7,SETFAM_1:def 1;
         end;
        hence A in F by A2,A9,A10,WAYBEL_7:25;
       end;
    end;
   assume
A11: for F being ultra Filter of BoolePoset [#]T
     ex x being Point of T st x is_a_convergence_point_of F, T;
      now let F be Subset-Family of T such that
A12:   F is centered closed;
     reconsider Y = F as Subset of BoolePoset X by A1;
     set L = BoolePoset X;
     set G = uparrow fininfs Y;
        now assume Bottom L in G;
       then consider x being Element of BoolePoset X such that
A13:     x <= Bottom L & x in fininfs Y by WAYBEL_0:def 16;
A14:     Bottom L = {} by YELLOW_1:18;
          fininfs Y = {"/\"(Z,L) where Z is finite Subset of Y: ex_inf_of Z,L}
         by WAYBEL_0:def 28;
       then consider Z being finite Subset of Y such that
A15:     x = "/\"(Z,L) & ex_inf_of Z,L by A13;
          Z c= the carrier of L by XBOOLE_1:1;
       then reconsider Z as Subset of L;
A16:     x = Bottom L by A13,YELLOW_5:22;
        then x <> Top L by WAYBEL_7:5;
then A17:     Z <> {} by A15,YELLOW_0:def 12;
        then meet Z <> {} by A12,COMPTS_1:def 2;
       hence contradiction by A14,A15,A16,A17,YELLOW_1:20;
      end;
      then G is proper by WAYBEL_7:8;
     then consider UF being Filter of L such that
A18:   G c= UF & UF is ultra by WAYBEL_7:30;
     consider x being Point of T such that
A19:   x is_a_convergence_point_of UF, T by A2,A11,A18;
A20:   F <> {} by A12,COMPTS_1:def 2;
        F c= G by WAYBEL_0:62;
then A21:   F c= UF by A18,XBOOLE_1:1;
        now let A be set; assume
A22:     A in F;
       then reconsider B = A as Subset of T;
A23:     now let C be Subset of T; assume C is open & x in C;
then A24:       C in UF & A in UF by A19,A21,A22,WAYBEL_7:def 5;
         then reconsider c = C, a = A as Element of L;
            a"/\"c in UF & UF is ultra Filter of L by A18,A24,WAYBEL_0:41;
          then a"/\"c <> {} by Th2;
         then A /\ C <> {} by YELLOW_1:17;
         hence A meets C by XBOOLE_0:def 7;
        end;
          B is closed by A12,A22,TOPS_2:def 2;
        then Cl B = B by PRE_TOPC:52;
       hence x in A by A23,PRE_TOPC:54;
      end;
     hence meet F <> {} by A20,SETFAM_1:def 1;
    end;
   hence thesis by COMPTS_1:13;
  end;

theorem
   for T being non empty TopSpace holds
    T is compact
  iff
    for F being proper Filter of BoolePoset [#]T
     ex x being Point of T st x is_a_cluster_point_of F, T
  proof let T be non empty TopSpace;
A1: the carrier of T = [#]T by PRE_TOPC:12;
   hereby assume
A2:   T is compact;
     let F be proper Filter of BoolePoset [#]T;
     reconsider G = F as proper Filter of BoolePoset [#]T;
     consider x being Point of T such that
A3:   x is_a_cluster_point_of a_net G by A2,Lm1;
     take x; thus x is_a_cluster_point_of F, T by A3,Th17;
    end;
   assume
A4: for F being proper Filter of BoolePoset [#]T
     ex x being Point of T st x is_a_cluster_point_of F, T;
      now let N be net of T such that N in NetUniv T;
     reconsider F = a_filter N as proper Filter of BoolePoset the carrier of T
       by A1;
     consider x being Point of T such that
A5:   x is_a_cluster_point_of F, T by A4;
     take x; thus x is_a_cluster_point_of N by A5,Th12;
    end;
   hence thesis by Lm2;
  end;

theorem Th35:
 for T being non empty TopSpace holds
    T is compact
  iff
    for N being net of T ex x being Point of T st
      x is_a_cluster_point_of N
  proof let T be non empty TopSpace;
   thus T is compact implies
    for N being net of T ex x being Point of T st
      x is_a_cluster_point_of N by Lm1;
   assume
      for N being net of T ex x being Point of T st
     x is_a_cluster_point_of N;
    then for N being net of T st N in NetUniv T
     ex x being Point of T st x is_a_cluster_point_of N;
   hence thesis by Lm2;
  end;

theorem
   for T being non empty TopSpace holds
    T is compact
  iff
    for N being net of T st N in NetUniv T
     ex x being Point of T st x is_a_cluster_point_of N by Lm1,Lm2;

definition
 let L be non empty 1-sorted;
 let N be transitive NetStr over L;
 cluster -> transitive (full SubNetStr of N);
 coherence
  proof let S be full SubNetStr of N;
      S is full SubRelStr of N by YELLOW_6:def 9;
   hence thesis;
  end;
end;

definition
 let L be non empty 1-sorted;
 let N be non empty directed NetStr over L;
 cluster strict non empty directed full SubNetStr of N;
 existence
  proof set S = the NetStr of N;
A1: N is SubNetStr of N & the RelStr of N = the RelStr of N &
    the RelStr of S = the RelStr of S & N is full SubRelStr of N
     by YELLOW_6:15,17;
    then the mapping of S = (the mapping of N)|the carrier of S &
    S is full SubRelStr of N by WAYBEL21:12,YELLOW_6:def 8;
   then reconsider S as strict non empty full SubNetStr of N
    by YELLOW_6:def 8,def 9;
      S is directed
     proof
         [#]N = the carrier of N & [#]S = the carrier of S &
       [#]N is directed by PRE_TOPC:12,WAYBEL_0:def 6;
      hence [#]S is directed by A1,WAYBEL_0:3;
     end;
   hence thesis;
  end;
end;

theorem
   for T being non empty TopSpace holds
    T is compact
  iff
    for N being net of T ex S being subnet of N st S is convergent
  proof let T be non empty TopSpace;
   hereby assume
A1:   T is compact;
     let N be net of T;
     consider x being Point of T such that
A2:   x is_a_cluster_point_of N by A1,Th35;
     consider S being subnet of N such that
A3:   x in Lim S by A2,WAYBEL_9:32;
     take S; thus S is convergent by A3,YELLOW_6:def 19;
    end;
   assume
A4: for N being net of T ex S being subnet of N st S is convergent;
      now let N be net of T;
     consider S being subnet of N such that
A5:   S is convergent by A4;
     consider x being Element of Lim S;
A6:   Lim S <> {} by A5,YELLOW_6:def 19;
     then x in Lim S;
     then reconsider x as Point of T;
     take x;
        x is_a_cluster_point_of S by A6,WAYBEL_9:29;
     hence x is_a_cluster_point_of N by WAYBEL_9:31;
    end;
   hence thesis by Th35;
  end;

definition
 let S be non empty 1-sorted;
 let N be non empty NetStr over S;
 attr N is Cauchy means
    for A being Subset of S holds N is_eventually_in A or N is_eventually_in A`
;
end;

definition
 let S be non empty 1-sorted;
 let F be ultra Filter of BoolePoset [#]S;
 cluster a_net F -> Cauchy;
 coherence
  proof let A be Subset of S;
A1: [#]S = the carrier of S by PRE_TOPC:12;
A2: ({}S)` = [#]S by PRE_TOPC:27;
then A3: A` = {}S implies A = [#]S;
      F is prime by WAYBEL_7:26;
    then A in F or (the carrier of S)\A in F by A1,WAYBEL_7:25;
    then (A is empty or A is non empty) & (A` is empty or A` is non empty) &
    A in F or A` in F by A1,PRE_TOPC:17;
   hence thesis by A1,A2,A3,Th16,YELLOW_6:29;
  end;
end;

theorem
   for T being non empty TopSpace holds
   T is compact
  iff
   for N being net of T st N is Cauchy holds N is convergent
  proof let T be non empty TopSpace;
   thus T is compact implies
    for N being net of T st N is Cauchy holds N is convergent
     proof assume
A1:    T is compact;
      let N be net of T such that
A2:    for A being Subset of T
        holds N is_eventually_in A or N is_eventually_in A`;
      consider x being Point of T such that
A3:    x is_a_cluster_point_of N by A1,Lm1;
         now let V be a_neighborhood of x;
        assume not N is_eventually_in V;
         then N is_eventually_in V` by A2;
        then consider i being Element of N such that
A4:      for j being Element of N st i <= j holds N.j in V` by WAYBEL_0:def 11;
           N is_often_in V by A3,WAYBEL_9:def 9;
        then consider j being Element of N such that
A5:      i <= j & N.j in V by WAYBEL_0:def 12;
           N.j in V` by A4,A5;
        hence contradiction by A5,YELLOW_6:10;
       end;
       then x in Lim N by YELLOW_6:def 18;
      hence N is convergent by YELLOW_6:def 19;
     end;
   assume
A6: for N being net of T st N is Cauchy holds N is convergent;
      now let F be ultra Filter of BoolePoset [#]T;
     consider x being Element of Lim a_net F;
        a_net F is convergent by A6;
then A7:   Lim a_net F <> {} by YELLOW_6:def 19;
      then x in Lim a_net F;
     then reconsider x as Point of T;
     take x; thus x is_a_convergence_point_of F, T by A7,Th18;
    end;
   hence T is compact by Th33;
  end;


Back to top