:: YELLOW19 semantic presentation

begin


theorem Th1: :: YELLOW19:1
for X being non empty set
for F being proper Filter of (BoolePoset X)
for A being set st A in F holds
not A is empty
proof
let X be non empty set ; ::_thesis: for F being proper Filter of (BoolePoset X)
for A being set st A in F holds
not A is empty
 Bottom (BoolePoset X) = {} by YELLOW_1:18;
hence  for F being proper Filter of (BoolePoset X)
for A being set st A in F holds
not A is empty by WAYBEL_7:4; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
let x be Point of T;
func NeighborhoodSystem x ->  Subset of (BoolePoset ([#] T)) equals :: YELLOW19:def 1
 {  A where A is a_neighborhood of x : verum  }  ;
coherence
  {  A where A is a_neighborhood of x : verum  }  is Subset of (BoolePoset ([#] T))
proof
set Y =  {  A where A is a_neighborhood of x : verum  }  ;
set X = the carrier of T;
  {  A where A is a_neighborhood of x : verum  }  c= bool the carrier of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  A where A is a_neighborhood of x : verum  }  or y in bool the carrier of T )
assume  y in  {  A where A is a_neighborhood of x : verum  }  ; ::_thesis: y in bool the carrier of T
then  ex A being a_neighborhood of x st y = A ;
hence  y in bool the carrier of T ; ::_thesis: verum
end;
hence   {  A where A is a_neighborhood of x : verum  }  is Subset of (BoolePoset ([#] T)) by WAYBEL_7:2; ::_thesis: verum
end;
end;

:: deftheorem  defines NeighborhoodSystem YELLOW19:def_1_:_
 for T being non empty TopSpace
for x being Point of T holds NeighborhoodSystem x =  {  A where A is a_neighborhood of x : verum  }  ;

theorem Th2: :: YELLOW19:2
for T being non empty TopSpace
for x being Point of T
for A being set holds
( A in NeighborhoodSystem x iff A is a_neighborhood of x )
proof
let T be non empty TopSpace; ::_thesis: for x being Point of T
for A being set holds
( A in NeighborhoodSystem x iff A is a_neighborhood of x )
let x be Point of T; ::_thesis: for A being set holds
( A in NeighborhoodSystem x iff A is a_neighborhood of x )
let B be set ; ::_thesis: ( B in NeighborhoodSystem x iff B is a_neighborhood of x )
 ( B in NeighborhoodSystem x iff ex A being a_neighborhood of x st B = A ) ;
hence  ( B in NeighborhoodSystem x iff B is a_neighborhood of x ) ; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
let x be Point of T;
cluster NeighborhoodSystem x ->  non empty proper filtered upper ;
coherence
 ( not NeighborhoodSystem x is empty & NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )
proof
set Y = NeighborhoodSystem x;
set X = the carrier of T;
set L = BoolePoset ([#] T);
set A0 = the a_neighborhood of x;
 the a_neighborhood of x in NeighborhoodSystem x ;
hence  not NeighborhoodSystem x is empty ; ::_thesis: ( NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )
 {} c= the carrier of T by XBOOLE_1:2;
then A1: {} in bool the carrier of T ;
 {} is not a_neighborhood of x by CONNSP_2:4;
then A2: not {} in NeighborhoodSystem x by Th2;
 the carrier of (BoolePoset the carrier of T) = bool the carrier of T by WAYBEL_7:2;
hence  NeighborhoodSystem x is proper by A1, A2, SUBSET_1:def_6; ::_thesis: ( NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered )
thus  NeighborhoodSystem x is upper ::_thesis: NeighborhoodSystem x is filtered
proof
let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def_20 ::_thesis: ( not a in NeighborhoodSystem x or not a <= b or b in NeighborhoodSystem x )
reconsider B = b as Subset of T by WAYBEL_7:2;
assume  a in NeighborhoodSystem x ; ::_thesis: ( not a <= b or b in NeighborhoodSystem x )
then reconsider A = a as a_neighborhood of x by Th2;
assume  a <= b ; ::_thesis: b in NeighborhoodSystem x
then  A c= B by YELLOW_1:2;
then A3: Int A c= Int B by TOPS_1:19;
 x in Int A by CONNSP_2:def_1;
then  b is a_neighborhood of x by A3, CONNSP_2:def_1;
hence  b in NeighborhoodSystem x ; ::_thesis: verum
end;
let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def_2 ::_thesis: ( not a in NeighborhoodSystem x or not b in NeighborhoodSystem x or ex b1 being Element of the carrier of (BoolePoset ([#] T)) st
( b1 in NeighborhoodSystem x & b1 <= a & b1 <= b ) )
assume that
A4: a in NeighborhoodSystem x and
A5: b in NeighborhoodSystem x ; ::_thesis: ex b1 being Element of the carrier of (BoolePoset ([#] T)) st
( b1 in NeighborhoodSystem x & b1 <= a & b1 <= b )
reconsider A = a, B = b as a_neighborhood of x by A4, A5, Th2;
A6: A /\ B is a_neighborhood of x by CONNSP_2:2;
then  A /\ B in NeighborhoodSystem x ;
then reconsider z = A /\ B as Element of (BoolePoset ([#] T)) ;
take  z ; ::_thesis: ( z in NeighborhoodSystem x & z <= a & z <= b )
A7: z c= B by XBOOLE_1:17;
 z c= A by XBOOLE_1:17;
hence  ( z in NeighborhoodSystem x & z <= a & z <= b ) by A6, A7, YELLOW_1:2; ::_thesis: verum
end;
end;

theorem Th3: :: YELLOW19:3
for T being non empty TopSpace
for 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; ::_thesis: for 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 )
let x be Point of T; ::_thesis: for F being upper Subset of (BoolePoset ([#] T)) holds
( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )
let F be upper Subset of (BoolePoset ([#] T)); ::_thesis: ( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F )
hereby  ::_thesis: ( NeighborhoodSystem x c= F implies x is_a_convergence_point_of F,T )
assume A1: x is_a_convergence_point_of F,T ; ::_thesis: NeighborhoodSystem x c= F
thus  NeighborhoodSystem x c= F ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in NeighborhoodSystem x or y in F )
assume  y in NeighborhoodSystem x ; ::_thesis: y in F
then reconsider y = y as a_neighborhood of x by Th2;
 x in Int y by CONNSP_2:def_1;
then A2: Int y in F by A1, WAYBEL_7:def_5;
 Int y c= y by TOPS_1:16;
hence  y in F by A2, WAYBEL_7:7; ::_thesis: verum
end;
end;
assume A3: NeighborhoodSystem x c= F ; ::_thesis: x is_a_convergence_point_of F,T
let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not x in A or A in F )
assume that
A4: A is open and
A5: x in A ; ::_thesis: A in F
 A is a_neighborhood of x by A4, A5, CONNSP_2:3;
then  A in NeighborhoodSystem x ;
hence  A in F by A3; ::_thesis: verum
end;

theorem :: YELLOW19:4
for T being non empty TopSpace
for x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x,T by Th3;

theorem :: YELLOW19:5
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 holds
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; ::_thesis: for A being Subset of T holds
( A is open iff for x being Point of T st x in A holds
for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds
A in F )
let A be Subset of T; ::_thesis: ( A is open iff for x being Point of T st x in A holds
for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds
A in F )
thus  ( A is open implies for x being Point of T st x in A holds
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; ::_thesis: ( ( for x being Point of T st x in A holds
for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds
A in F ) implies A is open )
assume A1: for x being Point of T st x in A holds
for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds
A in F ; ::_thesis: A is open
set x = the Element of A \ (Int A);
A2: Int A c= A by TOPS_1:16;
assume  not A is open ; ::_thesis: contradiction
then  not A c= Int A by A2, XBOOLE_0:def_10;
then A3: A \ (Int A) <> {} by XBOOLE_1:37;
then  the Element of A \ (Int A) in A \ (Int A) ;
then reconsider x = the Element of A \ (Int A) as Point of T ;
A4: x in A by A3, XBOOLE_0:def_5;
 x is_a_convergence_point_of NeighborhoodSystem x,T by Th3;
then  A in NeighborhoodSystem x by A1, A4;
then  A is a_neighborhood of x by Th2;
then  x in Int A by CONNSP_2:def_1;
hence  contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum
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: :: YELLOW19:def 2
 ex i being Element of N st it = rng the mapping of (N | i);
existence
 ex b1 being Subset of S ex i being Element of N st b1 = rng the mapping of (N | i)
proof
set i = the Element of N;
reconsider A = rng the mapping of (N | the Element of N) as Subset of S ;
take  A ; ::_thesis: ex i being Element of N st A = rng the mapping of (N | i)
take  the Element of N ; ::_thesis: A = rng the mapping of (N | the Element of N)
thus  A = rng the mapping of (N | the Element of N) ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Subset YELLOW19:def_2_:_
 for S being non empty 1-sorted
for N being non empty NetStr over S
for b3 being Subset of S holds
( b3 is Subset of S,N iff ex i being Element of N st b3 = rng the mapping of (N | i) );

theorem :: YELLOW19:6
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;

registration
let S be non empty 1-sorted ;
let N be non empty reflexive NetStr over S;
cluster  ->  non empty for Subset of S,N;
coherence
 for b1 being Subset of S,N holds not b1 is empty
proof
let A be Subset of S,N; ::_thesis: not A is empty
 ex i being Element of N st A = rng the mapping of (N | i) by Def2;
hence  not A is empty ; ::_thesis: verum
end;
end;

theorem Th7: :: YELLOW19:7
for S being non empty 1-sorted
for N being net of S
for i being Element of N
for 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 ; ::_thesis: for N being net of S
for i being Element of N
for 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 ) )
let N be net of S; ::_thesis: for i being Element of N
for 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 ) )
let i be Element of N; ::_thesis: for 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 ) )
let x be set ; ::_thesis: ( x in rng the mapping of (N | i) iff ex j being Element of N st
( i <= j & x = N . j ) )
A1: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def_1;
hereby  ::_thesis: ( ex j being Element of N st
( i <= j & x = N . j ) implies x in rng the mapping of (N | i) )
assume  x in rng the mapping of (N | i) ; ::_thesis: ex j being Element of N st
( i <= j & x = N . j )
then consider y being set  such that
A2: y in the carrier of (N | i) and
A3: x = the mapping of (N | i) . y by A1, FUNCT_1:def_3;
reconsider y = y as Element of (N | i) by A2;
consider j being Element of N such that
A4: j = y and
A5: i <= j by WAYBEL_9:def_7;
take j = j; ::_thesis: ( i <= j & x = N . j )
thus  i <= j by A5; ::_thesis: x = N . j
thus x = (N | i) . y by A3
.= N . j by A4, WAYBEL_9:16 ; ::_thesis: verum
end;
given j being Element of N such that A6: i <= j and
A7: x = N . j ; ::_thesis: x in rng the mapping of (N | i)
reconsider k = j as Element of (N | i) by A6, WAYBEL_9:def_7;
A8: x = (N | i) . k by A7, WAYBEL_9:16
.= the mapping of (N | i) . j ;
 j in the carrier of (N | i) by A6, WAYBEL_9:def_7;
hence  x in rng the mapping of (N | i) by A1, A8, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th8: :: YELLOW19:8
for S being non empty 1-sorted
for 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 ; ::_thesis: for N being net of S
for A being Subset of S,N holds N is_eventually_in A
let N be net of S; ::_thesis: for A being Subset of S,N holds N is_eventually_in A
let A be Subset of S,N; ::_thesis: N is_eventually_in A
consider i being Element of N such that
A1: A = rng the mapping of (N | i) by Def2;
take  i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not i <= b1 or N . b1 in A )
let j be Element of N; ::_thesis: ( not i <= j or N . j in A )
assume  i <= j ; ::_thesis: N . j in A
then reconsider j9 = j as Element of (N | i) by WAYBEL_9:def_7;
N . j = (N | i) . j9 by WAYBEL_9:16
.= the mapping of (N | i) . j9 ;
hence  N . j in A by A1, FUNCT_2:4; ::_thesis: verum
end;

theorem :: YELLOW19:9
for S being non empty 1-sorted
for N being net of S
for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds
ex B being Subset of S,N st B c= meet F
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S
for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds
ex B being Subset of S,N st B c= meet F
let N be net of S; ::_thesis: for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds
ex B being Subset of S,N st B c= meet F
defpred S1[ set , set ] means  ex i being Element of N st
( $2 = i & $1 = rng the mapping of (N | i) );
let F be non empty finite set ; ::_thesis: ( ( for A being Element of F holds A is Subset of S,N ) implies ex B being Subset of S,N st B c= meet F )
assume A1: for A being Element of F holds A is Subset of S,N ; ::_thesis: ex B being Subset of S,N st B c= meet F
A2: now__::_thesis:_for_x_being_set_st_x_in_F_holds_
ex_y_being_set_st_
(_y_in_the_carrier_of_N_&_S1[x,y]_)
let x be set ; ::_thesis: ( x in F implies ex y being set st
( y in the carrier of N & S1[x,y] ) )
assume  x in F ; ::_thesis: ex y being set st
( y in the carrier of N & S1[x,y] )
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 = y; ::_thesis: ( y in the carrier of N & S1[x,y] )
thus  y in the carrier of N ; ::_thesis: S1[x,y]
thus  S1[x,y] by A3; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = F & rng f c= the carrier of N ) and
A5: for x being set st x in F holds
S1[x,f . x] from FUNCT_1:sch_5(A2);
reconsider B = rng f as finite Subset of N by A4, FINSET_1:8;
 [#] N is directed by 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 Def2;
take  C ; ::_thesis: C c= meet F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in meet F )
A7: the carrier of (N | j) =  {  k where k is Element of N : j <= k  }  by WAYBEL_9:12;
assume  x in C ; ::_thesis: x in meet F
then consider y being set  such that
A8: y in dom the mapping of (N | j) and
A9: x = the mapping of (N | j) . y by FUNCT_1:def_3;
A10: y in the carrier of (N | j) by A8;
reconsider y = y as Element of (N | j) by A8;
consider k being Element of N such that
A11: y = k and
A12: j <= k by A10, A7;
now__::_thesis:_for_X_being_set_st_X_in_F_holds_
x_in_X
let X be set ; ::_thesis: ( X in F implies x in X )
assume A13: X in F ; ::_thesis: x in X
then consider i being Element of N such that
A14: f . X = i and
A15: X = rng the mapping of (N | i) by A5;
 i in B by A4, A13, A14, FUNCT_1:def_3;
then  i <= j by A6, LATTICE3:def_9;
then  i <= k by A12, ORDERS_2:3;
then  y in  {  l where l is Element of N : i <= l  }  by A11;
then reconsider z = y as Element of (N | i) by WAYBEL_9:12;
x = (N | j) . y by A9
.= N . k by A11, WAYBEL_9:16
.= (N | i) . z by A11, WAYBEL_9:16
.= the mapping of (N | i) . z ;
hence  x in X by A15, FUNCT_2:4; ::_thesis: verum
end;
hence  x in meet F by SETFAM_1:def_1; ::_thesis: verum
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 :: YELLOW19:def 3
 {  A where A is Subset of T : N is_eventually_in A  }  ;
coherence
  {  A where A is Subset of T : N is_eventually_in A  }  is Subset of (BoolePoset ([#] T))
proof
set X = the carrier of T;
set F =  {  A where A is Subset of T : N is_eventually_in A  }  ;
A1:  {  A where A is Subset of T : N is_eventually_in A  }  c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  A where A is Subset of T : N is_eventually_in A  }  or x in bool the carrier of T )
assume  x in  {  A where A is Subset of T : N is_eventually_in A  }  ; ::_thesis: x in bool the carrier of T
then  ex A being Subset of T st
( x = A & N is_eventually_in A ) ;
hence  x in bool the carrier of T ; ::_thesis: verum
end;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4
.= RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1 ;
hence   {  A where A is Subset of T : N is_eventually_in A  }  is Subset of (BoolePoset ([#] T)) by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines a_filter YELLOW19:def_3_:_
 for T being non empty 1-sorted
for N being non empty NetStr over T holds a_filter N =  {  A where A is Subset of T : N is_eventually_in A  }  ;

theorem Th10: :: YELLOW19:10
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 ; ::_thesis: 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 ) )
let N be non empty NetStr over T; ::_thesis: for A being set holds
( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) )
let B be set ; ::_thesis: ( B in a_filter N iff ( N is_eventually_in B & B is Subset of T ) )
 ( B in a_filter N iff ex A being Subset of T st
( B = A & N is_eventually_in A ) ) ;
hence  ( B in a_filter N iff ( N is_eventually_in B & B is Subset of T ) ) ; ::_thesis: verum
end;

registration
let T be non empty 1-sorted ;
let N be non empty NetStr over T;
cluster a_filter N ->  non empty upper ;
coherence
 ( not a_filter N is empty & a_filter N is upper )
proof
set X = the carrier of T;
set L = BoolePoset ([#] T);
set F = a_filter N;
 N is_eventually_in [#] T
proof
set i = the Element of N;
take  the Element of N ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not the Element of N <= b1 or N . b1 in [#] T )
thus  for b1 being Element of the carrier of N holds
( not the Element of N <= b1 or N . b1 in [#] T ) ; ::_thesis: verum
end;
hence  not a_filter N is empty by Th10; ::_thesis: a_filter N is upper
let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def_20 ::_thesis: ( not a in a_filter N or not a <= b or b in a_filter N )
assume  a in a_filter N ; ::_thesis: ( not a <= b or b in a_filter N )
then A1: N is_eventually_in a by Th10;
assume  a <= b ; ::_thesis: b in a_filter N
then  a c= b by YELLOW_1:2;
then A2: N is_eventually_in b by A1, WAYBEL_0:8;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4
.= RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1 ;
hence  b in a_filter N by A2; ::_thesis: verum
end;
end;

registration
let T be non empty 1-sorted ;
let N be net of T;
cluster a_filter N ->  proper filtered ;
coherence
 ( a_filter N is proper & a_filter N is filtered )
proof
set X = the carrier of T;
set L = BoolePoset ([#] T);
set F = a_filter N;
A1: BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4
.= RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1 ;
now__::_thesis:_(_{}_c=_the_carrier_of_T_&_not_{}_in_a_filter_N_)
thus  {} c= the carrier of T by XBOOLE_1:2; ::_thesis: not {} in a_filter N
assume  {} in a_filter N ; ::_thesis: contradiction
then  N is_eventually_in {} by Th10;
then consider i being Element of N such that
A2: for j being Element of N st i <= j holds
N . j in {} by WAYBEL_0:def_11;
 ex j being Element of N st
( i <= j & i <= j ) by YELLOW_6:def_3;
hence  contradiction by A2; ::_thesis: verum
end;
then  a_filter N <> bool the carrier of T ;
hence  a_filter N is proper by A1, SUBSET_1:def_6; ::_thesis: a_filter N is filtered
let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def_2 ::_thesis: ( not a in a_filter N or not b in a_filter N or ex b1 being Element of the carrier of (BoolePoset ([#] T)) st
( b1 in a_filter N & b1 <= a & b1 <= b ) )
assume that
A3: a in a_filter N and
A4: b in a_filter N ; ::_thesis: ex b1 being Element of the carrier of (BoolePoset ([#] T)) st
( b1 in a_filter N & b1 <= a & b1 <= b )
 N is_eventually_in a by A3, Th10;
then consider i1 being Element of N such that
A5: for j being Element of N st i1 <= j holds
N . j in a by WAYBEL_0:def_11;
 N is_eventually_in b by A4, Th10;
then consider i2 being Element of N such that
A6: for j being Element of N st i2 <= j holds
N . j in b by WAYBEL_0:def_11;
take z = a "/\" b; ::_thesis: ( z in a_filter N & z <= a & z <= b )
A7: z = a /\ b by YELLOW_1:17;
then A8: z c= b by XBOOLE_1:17;
consider i being Element of N such that
A9: i1 <= i and
A10: i2 <= i by YELLOW_6:def_3;
now__::_thesis:_for_j_being_Element_of_N_st_i_<=_j_holds_
N_._j_in_a_/\_b
let j be Element of N; ::_thesis: ( i <= j implies N . j in a /\ b )
assume A11: i <= j ; ::_thesis: N . j in a /\ b
then A12: N . j in b by A6, A10, ORDERS_2:3;
 N . j in a by A5, A9, A11, ORDERS_2:3;
hence  N . j in a /\ b by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
then  N is_eventually_in z by A7, WAYBEL_0:def_11;
hence  z in a_filter N by A1; ::_thesis: ( z <= a & z <= b )
 z c= a by A7, XBOOLE_1:17;
hence  ( z <= a & z <= b ) by A8, YELLOW_1:2; ::_thesis: verum
end;
end;

theorem Th11: :: YELLOW19:11
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; ::_thesis: 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 )
let N be net of T; ::_thesis: 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 )
set F = a_filter N;
let x be Point of T; ::_thesis: ( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T )
thus  ( x is_a_cluster_point_of N implies x is_a_cluster_point_of a_filter N,T ) ::_thesis: ( x is_a_cluster_point_of a_filter N,T implies x is_a_cluster_point_of N )
proof
assume A1: for O being a_neighborhood of x holds N is_often_in O ; :: according to WAYBEL_9:def_9 ::_thesis: x is_a_cluster_point_of a_filter N,T
let A be Subset of T; :: according to WAYBEL_7:def_4 ::_thesis: ( not A is open or not x in A or for b1 being set holds
( not b1 in a_filter N or not A misses b1 ) )
assume that
A2: A is open and
A3: x in A ; ::_thesis: for b1 being set holds
( not b1 in a_filter N or not A misses b1 )
let B be set ; ::_thesis: ( not B in a_filter N or not A misses B )
assume  B in a_filter N ; ::_thesis: not A misses B
then  N is_eventually_in B by Th10;
then consider i being Element of N such that
A4: for j being Element of N st i <= j holds
N . j in B by WAYBEL_0:def_11;
 A is a_neighborhood of x by A2, A3, CONNSP_2:3;
then  N is_often_in A by A1;
then  ex j being Element of N st
( i <= j & N . j in A ) by WAYBEL_0:def_12;
then  ex a being Point of T st
( a in B & a in A ) by A4;
hence  not A misses B by XBOOLE_0:3; ::_thesis: verum
end;
assume A5: for A being Subset of T st A is open & x in A holds
for B being set st B in a_filter N holds
A meets B ; :: according to WAYBEL_7:def_4 ::_thesis: x is_a_cluster_point_of N
let O be a_neighborhood of x; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in O
let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of N st
( i <= b1 & N . b1 in O )
reconsider B = rng the mapping of (N | i) as Subset of T,N by Def2;
 N is_eventually_in B by Th8;
then A6: B in a_filter N ;
 x in Int O by CONNSP_2:def_1;
then  Int O meets B by A5, A6;
then consider x being set  such that
A7: x in Int O and
A8: x in B by XBOOLE_0:3;
consider j being Element of N such that
A9: i <= j and
A10: x = N . j by A8, Th7;
take  j ; ::_thesis: ( i <= j & N . j in O )
 Int O c= O by TOPS_1:16;
hence  ( i <= j & N . j in O ) by A7, A9, A10; ::_thesis: verum
end;

theorem Th12: :: YELLOW19:12
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; ::_thesis: 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 )
let N be net of T; ::_thesis: for x being Point of T holds
( x in Lim N iff x is_a_convergence_point_of a_filter N,T )
set F = a_filter N;
let x be Point of T; ::_thesis: ( x in Lim N iff x is_a_convergence_point_of a_filter N,T )
thus  ( x in Lim N implies x is_a_convergence_point_of a_filter N,T ) ::_thesis: ( x is_a_convergence_point_of a_filter N,T implies x in Lim N )
proof
assume A1: x in Lim N ; ::_thesis: x is_a_convergence_point_of a_filter N,T
let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not x in A or A in a_filter N )
assume that
A2: A is open and
A3: x in A ; ::_thesis: A in a_filter N
 A is a_neighborhood of x by A2, A3, CONNSP_2:3;
then  N is_eventually_in A by A1, YELLOW_6:def_15;
hence  A in a_filter N ; ::_thesis: verum
end;
assume A4: for A being Subset of T st A is open & x in A holds
A in a_filter N ; :: according to WAYBEL_7:def_5 ::_thesis: x in Lim N
now__::_thesis:_for_O_being_a_neighborhood_of_x_holds_N_is_eventually_in_O
let O be a_neighborhood of x; ::_thesis: N is_eventually_in O
 x in Int O by CONNSP_2:def_1;
then  Int O in a_filter N by A4;
then A5: N is_eventually_in Int O by Th10;
 Int O c= O by TOPS_1:16;
hence  N is_eventually_in O by A5, WAYBEL_0:8; ::_thesis: verum
end;
hence  x in Lim N by YELLOW_6:def_15; ::_thesis: verum
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 ->  non empty strict NetStr over L means :Def4: :: YELLOW19:def 4
( 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
 ex b1 being non empty strict NetStr over L st
( the carrier of b1 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  & ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) )
proof
deffunc H1( set ) ->  set = $1 `1 ;
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:8;
reconsider f = f as Subset of L ;
consider a being Element of L such that
A1: a in f by SUBSET_1:4;
reconsider a = a as Element of L ;
 [a,f] in  {  [a,f] where a is Element of L, f is Element of F : a in f  }  by A1;
then reconsider S =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  as non empty set ;
defpred S1[ 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 S1[x,y] ) from RELSET_1:sch_2();
A3: for x being set st x in S holds
H1(x) in the carrier of L
proof
let x be set ; ::_thesis: ( x in S implies H1(x) in the carrier of L )
assume  x in S ; ::_thesis: H1(x) in the carrier of L
then consider a being Element of L, f being Element of F such that
A4: x = [a,f] and
 a in f ;
 [a,f] `1 = a ;
hence  H1(x) in the carrier of L by A4; ::_thesis: verum
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 = H1(x) from FUNCT_2:sch_2(A3);
take N = NetStr(# S,R,h #); ::_thesis: ( the carrier of N =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  & ( for i, j being Element of N holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of N holds N . i = i `1 ) )
 for i, j being Element of N holds
( i <= j iff j `2 c= i `2 )
proof
let i, j be Element of N; ::_thesis: ( i <= j iff j `2 c= i `2 )
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  ( i <= j iff j `2 c= i `2 ) by ORDERS_2:def_5; ::_thesis: verum
end;
hence  ( the carrier of N =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  & ( for i, j being Element of N holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of N holds N . i = i `1 ) ) by A5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict NetStr over L st the carrier of b1 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  & ( for i, j being Element of b1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) & the carrier of b2 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  & ( for i, j being Element of b2 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b2 holds b2 . i = i `1 ) holds
b1 = b2
proof
set S =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  ;
let it1, it2 be non empty strict NetStr over L; ::_thesis: ( the carrier of it1 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  & ( for i, j being Element of it1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it1 holds it1 . i = i `1 ) & the carrier of it2 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  & ( for i, j being Element of it2 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it2 holds it2 . i = i `1 ) implies it1 = it2 )
assume that
A6: the carrier of it1 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  and
A7: for i, j being Element of it1 holds
( i <= j iff j `2 c= i `2 ) and
A8: for i being Element of it1 holds it1 . i = i `1 and
A9: the carrier of it2 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  and
A10: for i, j being Element of it2 holds
( i <= j iff j `2 c= i `2 ) and
A11: for i being Element of it2 holds it2 . i = i `1 ; ::_thesis: it1 = it2
A12: 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 ; ::_thesis: ( [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 )
hereby  ::_thesis: ( [x,y] in the InternalRel of it2 implies [x,y] in the InternalRel of it1 )
assume A13: [x,y] in the InternalRel of it1 ; ::_thesis: [x,y] in the InternalRel of it2
then reconsider i = x, j = y as Element of it1 by ZFMISC_1:87;
reconsider i9 = x, j9 = y as Element of it2 by A6, A9, A13, ZFMISC_1:87;
 i <= j by A13, ORDERS_2:def_5;
then  j9 `2 c= i9 `2 by A7;
then  i9 <= j9 by A10;
hence  [x,y] in the InternalRel of it2 by ORDERS_2:def_5; ::_thesis: verum
end;
assume A14: [x,y] in the InternalRel of it2 ; ::_thesis: [x,y] in the InternalRel of it1
then reconsider i = x, j = y as Element of it2 by ZFMISC_1:87;
reconsider i9 = x, j9 = y as Element of it1 by A6, A9, A14, ZFMISC_1:87;
 i <= j by A14, ORDERS_2:def_5;
then  j9 `2 c= i9 `2 by A10;
then  i9 <= j9 by A7;
hence  [x,y] in the InternalRel of it1 by ORDERS_2:def_5; ::_thesis: verum
end;
 the mapping of it1 = the mapping of it2
proof
reconsider f2 = the mapping of it2 as Function of  {  [a,f] where a is Element of L, f is Element of F : a in f  }  , the carrier of L by A9;
reconsider f1 = the mapping of it1 as Function of  {  [a,f] where a is Element of L, f is Element of F : a in f  }  , the carrier of L by A6;
 for x being set st x in  {  [a,f] where a is Element of L, f is Element of F : a in f  }  holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in  {  [a,f] where a is Element of L, f is Element of F : a in f  }  implies f1 . x = f2 . x )
assume A15: x in  {  [a,f] where a is Element of L, f is Element of F : a in f  }  ; ::_thesis: f1 . x = f2 . x
then reconsider x1 = x as Element of it1 by A6;
reconsider x2 = x as Element of it2 by A9, A15;
reconsider x = x as Element of  {  [a,f] where a is Element of L, f is Element of F : a in f  }  by A15;
f1 . x = it1 . x1
.= x1 `1 by A8
.= it2 . x2 by A11 ;
hence  f1 . x = f2 . x ; ::_thesis: verum
end;
hence  the mapping of it1 = the mapping of it2 by FUNCT_2:12; ::_thesis: verum
end;
hence  it1 = it2 by A6, A9, A12, RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines a_net YELLOW19:def_4_:_
 for L being non empty 1-sorted
for O being non empty Subset of L
for F being Filter of (BoolePoset O)
for b4 being non empty strict NetStr over L holds
( b4 = a_net F iff ( the carrier of b4 =  {  [a,f] where a is Element of L, f is Element of F : a in f  }  & ( for i, j being Element of b4 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b4 holds b4 . i = i `1 ) ) );

registration
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 ->  non empty reflexive transitive strict ;
coherence
 ( a_net F is reflexive & a_net F is transitive )
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 ; ::_thesis: ( 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) implies [x,z] in the InternalRel of (a_net F) )
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) ; ::_thesis: [x,z] in the InternalRel of (a_net F)
reconsider k = z as Element of (a_net F) by A3;
reconsider j = y as Element of (a_net F) by A2;
 j <= k by A5, ORDERS_2:def_5;
then A6: k `2 c= j `2 by Def4;
reconsider i = x as Element of (a_net F) by A1;
 i <= j by A4, ORDERS_2:def_5;
then  j `2 c= i `2 by Def4;
then  k `2 c= i `2 by A6, XBOOLE_1:1;
then  i <= k by Def4;
hence  [x,z] in the InternalRel of (a_net F) by ORDERS_2:def_5; ::_thesis: verum
end;
then A7: 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 be set ; ::_thesis: ( x in the carrier of (a_net F) implies [x,x] in the InternalRel of (a_net F) )
assume  x in the carrier of (a_net F) ; ::_thesis: [x,x] in the InternalRel 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  [x,x] in the InternalRel of (a_net F) by ORDERS_2:def_5; ::_thesis: verum
end;
then  the InternalRel of (a_net F) is_reflexive_in the carrier of (a_net F) by RELAT_2:def_1;
hence  ( a_net F is reflexive & a_net F is transitive ) by A7, ORDERS_2:def_2, ORDERS_2:def_3; ::_thesis: verum
end;
end;

registration
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 ->  non empty strict directed ;
coherence
 a_net F is directed
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) holds
ex z being Element of (a_net F) st
( z in [#] (a_net F) & x <= z & y <= z )
proof
let x, y be Element of (a_net F); ::_thesis: ( x in [#] (a_net F) & y in [#] (a_net F) implies ex z being Element of (a_net F) st
( z in [#] (a_net F) & x <= z & y <= z ) )
assume that
 x in [#] (a_net F) and
 y in [#] (a_net F) ; ::_thesis: ex z being Element of (a_net F) st
( z in [#] (a_net F) & x <= z & y <= z )
 x in the carrier of (a_net F) ;
then  x in  {  [a,f] where a is Element of L, f is Element of F : a in f  }  by Def4;
then consider a being Element of L, f being Element of F such that
A1: x = [a,f] and
 a in f ;
reconsider f = f as Element of (BoolePoset O) ;
 y in the carrier of (a_net F) ;
then  y in  {  [a,f] where a is Element of L, f is Element of F : a in f  }  by Def4;
then consider b being Element of L, g being Element of F such that
A2: y = [b,g] and
 b in g ;
reconsider g = g as Element of (BoolePoset O) ;
reconsider h = f "/\" g as Element of F by WAYBEL_0:41;
set s = the Element of h;
A3: h c= O by WAYBEL_8:26;
 not Bottom (BoolePoset O) in F by WAYBEL_7:4;
then  not {} in F by YELLOW_1:18;
then A4: h <> {} ;
then  the Element of h in h ;
then  the Element of h in O by A3;
then reconsider s = the Element of h as Element of L ;
 [s,h] in  {  [a,f] where a is Element of L, f is Element of F : a in f  }  by A4;
then reconsider z = [s,h] as Element of (a_net F) by Def4;
reconsider i = x, j = y, k = z as Element of (a_net F) ;
A5: [b,g] `2 = g ;
take  z ; ::_thesis: ( z in [#] (a_net F) & x <= z & y <= z )
A6: [s,h] `2 = h ;
 f /\ g c= g by XBOOLE_1:17;
then A7: h c= g by YELLOW_1:17;
 f /\ g c= f by XBOOLE_1:17;
then A8: h c= f by YELLOW_1:17;
 [a,f] `2 = f ;
hence  ( z in [#] (a_net F) & x <= z & y <= z ) by A5, A6, A8, A7, Def4, A1, A2; ::_thesis: verum
end;
then  [#] (a_net F) is directed by WAYBEL_0:def_1;
hence  a_net F is directed by WAYBEL_0:def_6; ::_thesis: verum
end;
end;

theorem Th13: :: YELLOW19:13
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 ; ::_thesis: for F being Filter of (BoolePoset ([#] T)) holds F \ {{}} = a_filter (a_net F)
let F be Filter of (BoolePoset ([#] T)); ::_thesis: F \ {{}} = a_filter (a_net F)
set X = a_filter (a_net F);
A1: the carrier of (a_net F) =  {  [a,f] where a is Element of T, f is Element of F : a in f  }  by Def4;
A2: BoolePoset ([#] T) = InclPoset (bool ([#] T)) by YELLOW_1:4;
thus  F \ {{}} c= a_filter (a_net F) :: according to XBOOLE_0:def_10 ::_thesis: a_filter (a_net F) c= F \ {{}}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F \ {{}} or x in a_filter (a_net F) )
assume A3: x in F \ {{}} ; ::_thesis: x in a_filter (a_net F)
then reconsider A = x as Subset of T by A2, YELLOW_1:1;
set a = the Element of A;
 not x in {{}} by A3, XBOOLE_0:def_5;
then A4: A <> {} by TARSKI:def_1;
then  the Element of A in A ;
then reconsider a = the Element of A as Element of T ;
 x in F by A3, XBOOLE_0:def_5;
then  [a,A] in the carrier of (a_net F) by A1, A4;
then reconsider i = [a,A] as Element of (a_net F) ;
 a_net F is_eventually_in A
proof
take  i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (a_net F) holds
( not i <= b1 or (a_net F) . b1 in A )
let j be Element of (a_net F); ::_thesis: ( not i <= j or (a_net F) . j in A )
A5: i `2 = A by MCART_1:7;
A6: (a_net F) . j = j `1 by Def4;
assume  i <= j ; ::_thesis: (a_net F) . j in A
then A7: j `2 c= i `2 by Def4;
 j in the carrier of (a_net F) ;
then consider a being Element of T, f being Element of F such that
A8: j = [a,f] and
A9: a in f by A1;
A10: j `1 = a by A8, MCART_1:7;
 j `2 = f by A8, MCART_1:7;
hence  (a_net F) . j in A by A9, A7, A6, A5, A10; ::_thesis: verum
end;
hence  x in a_filter (a_net F) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a_filter (a_net F) or x in F \ {{}} )
assume A11: x in a_filter (a_net F) ; ::_thesis: x in F \ {{}}
then  a_net F is_eventually_in x by Th10;
then consider i being Element of (a_net F) such that
A12: 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
A13: i = [a,f] and
A14: a in f by A1;
A15: the carrier of (BoolePoset ([#] T)) = bool ([#] T) by A2, YELLOW_1:1;
A16: f c= x
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f or x in x )
assume A17: x in f ; ::_thesis: x in x
then reconsider b = x as Element of T by A15;
 [b,f] in the carrier of (a_net F) by A1, A17;
then reconsider j = [b,f] as Element of (a_net F) ;
A18: j `2 = f by MCART_1:7;
 j `1 = b by MCART_1:7;
then A19: (a_net F) . j = b by Def4;
 i `2 = f by A13, MCART_1:7;
then  i <= j by A18, Def4;
hence  x in x by A12, A19; ::_thesis: verum
end;
 x is Subset of T by A11, Th10;
then A20: x in F by A16, WAYBEL_7:7;
 not x in {{}} by A14, A16, TARSKI:def_1;
hence  x in F \ {{}} by A20, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th14: :: YELLOW19:14
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 ; ::_thesis: for F being proper Filter of (BoolePoset ([#] T)) holds F = a_filter (a_net F)
let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: F = a_filter (a_net F)
 not {} in F by Th1;
then  F \ {{}} = F by ZFMISC_1:57;
hence  F = a_filter (a_net F) by Th13; ::_thesis: verum
end;

theorem Th15: :: YELLOW19:15
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 ; ::_thesis: 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 )
let F be Filter of (BoolePoset ([#] T)); ::_thesis: for A being non empty Subset of T holds
( A in F iff a_net F is_eventually_in A )
let B be non empty Subset of T; ::_thesis: ( B in F iff a_net F is_eventually_in B )
A1: ( B in F iff B in F \ {{}} ) by ZFMISC_1:56;
 F \ {{}} = a_filter (a_net F) by Th13;
hence  ( B in F iff a_net F is_eventually_in B ) by A1, Th10; ::_thesis: verum
end;

theorem Th16: :: YELLOW19:16
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; ::_thesis: 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 )
let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: 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 )
 F = a_filter (a_net F) by Th14;
hence  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 ) by Th11; ::_thesis: verum
end;

theorem Th17: :: YELLOW19:17
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; ::_thesis: 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 )
let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: for x being Point of T holds
( x in Lim (a_net F) iff x is_a_convergence_point_of F,T )
 F = a_filter (a_net F) by Th14;
hence  for x being Point of T holds
( x in Lim (a_net F) iff x is_a_convergence_point_of F,T ) by Th12; ::_thesis: verum
end;

theorem Th18: :: YELLOW19:18
for T being non empty TopSpace
for x being Point of T
for A being Subset of T st x in Cl A holds
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; ::_thesis: for x being Point of T
for A being Subset of T st x in Cl A holds
for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A
let x be Point of T; ::_thesis: for A being Subset of T st x in Cl A holds
for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A
let A be Subset of T; ::_thesis: ( x in Cl A implies for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A )
assume A1: x in Cl A ; ::_thesis: for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A
let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: ( F = NeighborhoodSystem x implies a_net F is_often_in A )
assume A2: F = NeighborhoodSystem x ; ::_thesis: a_net F is_often_in A
set N = a_net F;
let i be Element of (a_net F); :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of (a_net F) st
( i <= b1 & (a_net F) . b1 in A )
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;
 i in the carrier of (a_net F) ;
then consider a being Element of T, f being Element of F such that
A4: i = [a,f] and
 a in f by A3;
reconsider f = f as a_neighborhood of x by A2, Th2;
A5: i `2 = f by A4, MCART_1:7;
 f meets A by A1, CONNSP_2:27;
then consider b being set  such that
A6: b in f and
A7: b in A by XBOOLE_0:3;
reconsider b = b as Element of T by A6;
 [b,f] in the carrier of (a_net F) by A3, A6;
then reconsider j = [b,f] as Element of (a_net F) ;
take  j ; ::_thesis: ( i <= j & (a_net F) . j in A )
A8: j `1 = b by MCART_1:7;
 j `2 = f by MCART_1:7;
hence  ( i <= j & (a_net F) . j in A ) by A7, A5, A8, Def4; ::_thesis: verum
end;

theorem Th19: :: YELLOW19:19
for T being non empty 1-sorted
for A being set
for N being net of T st N is_eventually_in A holds
for S being subnet of N holds S is_eventually_in A
proof
let T be non empty 1-sorted ; ::_thesis: for A being set
for N being net of T st N is_eventually_in A holds
for S being subnet of N holds S is_eventually_in A
let A be set ; ::_thesis: for N being net of T st N is_eventually_in A holds
for S being subnet of N holds S is_eventually_in A
let N be net of T; ::_thesis: ( N is_eventually_in A implies for S being subnet of N holds S is_eventually_in A )
given i being Element of N such that A1: for j being Element of N st i <= j holds
N . j in A ; :: according to WAYBEL_0:def_11 ::_thesis: for S being subnet of N holds S is_eventually_in A
let S be subnet of N; ::_thesis: S is_eventually_in A
consider f being Function 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_9;
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 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of S holds
( not n <= b1 or S . b1 in A )
let p be Element of S; ::_thesis: ( not n <= p or S . p in A )
assume  n <= p ; ::_thesis: S . p in A
then  N . (f . p) in A by A1, A4;
hence  S . p in A by A2, FUNCT_2:15; ::_thesis: verum
end;

theorem Th20: :: YELLOW19:20
for T being non empty TopSpace
for 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; ::_thesis: for 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
let F, G, x be set ; ::_thesis: ( F c= G & x is_a_convergence_point_of F,T implies x is_a_convergence_point_of G,T )
assume that
A1: F c= G and
A2: for A being Subset of T st A is open & x in A holds
A in F ; :: according to WAYBEL_7:def_5 ::_thesis: x is_a_convergence_point_of G,T
let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not x in A or A in G )
assume that
A3: A is open and
A4: x in A ; ::_thesis: A in G
 A in F by A2, A3, A4;
hence  A in G by A1; ::_thesis: verum
end;

theorem Th21: :: YELLOW19:21
for T being non empty TopSpace
for 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; ::_thesis: for 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 ) )
let A be Subset of T; ::_thesis: 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 ) )
let x be Point of T; ::_thesis: ( x in Cl A iff ex N being net of T st
( N is_eventually_in A & x is_a_cluster_point_of N ) )
reconsider F = NeighborhoodSystem x as proper Filter of (BoolePoset ([#] T)) ;
hereby  ::_thesis: ( ex N being net of T st
( N is_eventually_in A & x is_a_cluster_point_of N ) implies x in Cl A )
assume  x in Cl A ; ::_thesis: ex N9 being net of T st
( N9 is_eventually_in A & x is_a_cluster_point_of N9 )
then reconsider N = (a_net F) " A as subnet of a_net F by Th18, YELLOW_6:22;
reconsider N9 = N as net of T ;
take N9 = N9; ::_thesis: ( N9 is_eventually_in A & x is_a_cluster_point_of N9 )
thus  N9 is_eventually_in A by YELLOW_6:23; ::_thesis: x is_a_cluster_point_of N9
 x is_a_convergence_point_of F,T by Th3;
then A1: x in Lim (a_net F) by Th17;
 Lim (a_net F) c= Lim N by YELLOW_6:32;
hence  x is_a_cluster_point_of N9 by A1, WAYBEL_9:29; ::_thesis: verum
end;
given N being net of T such that A2: N is_eventually_in A and
A3: x is_a_cluster_point_of N ; ::_thesis: x in Cl A
consider i being Element of N such that
A4: for j being Element of N st i <= j holds
N . j in A by A2, WAYBEL_0:def_11;
now__::_thesis:_for_G_being_Subset_of_T_st_G_is_open_&_x_in_G_holds_
A_meets_G
let G be Subset of T; ::_thesis: ( G is open & x in G implies A meets G )
assume that
A5: G is open and
A6: x in G ; ::_thesis: A meets G
 Int G = G by A5, TOPS_1:23;
then  G is a_neighborhood of x by A6, CONNSP_2:def_1;
then  N is_often_in G by A3, WAYBEL_9:def_9;
then consider j being Element of N such that
A7: i <= j and
A8: N . j in G by WAYBEL_0:def_12;
 N . j in A by A4, A7;
hence  A meets G by A8, XBOOLE_0:3; ::_thesis: verum
end;
hence  x in Cl A by PRE_TOPC:def_7; ::_thesis: verum
end;

theorem Th22: :: YELLOW19:22
for T being non empty TopSpace
for 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; ::_thesis: for 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 ) )
let A be Subset of T; ::_thesis: 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 ) )
let x be Point of T; ::_thesis: ( x in Cl A iff ex N being convergent net of T st
( N is_eventually_in A & x in Lim N ) )
hereby  ::_thesis: ( ex N being convergent net of T st
( N is_eventually_in A & x in Lim N ) implies x in Cl A )
assume  x in Cl A ; ::_thesis: ex S being convergent net of T st
( S is_eventually_in A & x in Lim S )
then consider N being net of T such that
A1: N is_eventually_in A and
A2: x is_a_cluster_point_of N by Th21;
consider S being subnet of N such that
A3: x in Lim S by A2, WAYBEL_9:32;
reconsider S = S as convergent net of T by A3, YELLOW_6:def_16;
take S = S; ::_thesis: ( S is_eventually_in A & x in Lim S )
thus  S is_eventually_in A by A1, Th19; ::_thesis: x in Lim S
thus  x in Lim S by A3; ::_thesis: verum
end;
given N being convergent net of T such that A4: N is_eventually_in A and
A5: x in Lim N ; ::_thesis: x in Cl A
 x is_a_cluster_point_of N by A5, WAYBEL_9:29;
hence  x in Cl A by A4, Th21; ::_thesis: verum
end;

theorem :: YELLOW19:23
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for N being net of T st N is_eventually_in A holds
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; ::_thesis: for A being Subset of T holds
( A is closed iff for N being net of T st N is_eventually_in A holds
for x being Point of T st x is_a_cluster_point_of N holds
x in A )
let A be Subset of T; ::_thesis: ( A is closed iff for N being net of T st N is_eventually_in A holds
for x being Point of T st x is_a_cluster_point_of N holds
x in A )
 ( A is closed iff Cl A = A ) by PRE_TOPC:22;
hence  ( A is closed implies for N being net of T st N is_eventually_in A holds
for x being Point of T st x is_a_cluster_point_of N holds
x in A ) by Th21; ::_thesis: ( ( for N being net of T st N is_eventually_in A holds
for x being Point of T st x is_a_cluster_point_of N holds
x in A ) implies A is closed )
assume A1: for N being net of T st N is_eventually_in A holds
for x being Point of T st x is_a_cluster_point_of N holds
x in A ; ::_thesis: A is closed
 A = Cl A
proof
thus  A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A )
assume A2: x in Cl A ; ::_thesis: x in 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, Th21;
hence  x in A by A1; ::_thesis: verum
end;
hence  A is closed ; ::_thesis: verum
end;

theorem :: YELLOW19:24
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for N being convergent net of T st N is_eventually_in A holds
for x being Point of T st x in Lim N holds
x in A )
proof
let T be non empty TopSpace; ::_thesis: for A being Subset of T holds
( A is closed iff for N being convergent net of T st N is_eventually_in A holds
for x being Point of T st x in Lim N holds
x in A )
let A be Subset of T; ::_thesis: ( A is closed iff for N being convergent net of T st N is_eventually_in A holds
for x being Point of T st x in Lim N holds
x in A )
 ( A is closed iff Cl A = A ) by PRE_TOPC:22;
hence  ( A is closed implies for N being convergent net of T st N is_eventually_in A holds
for x being Point of T st x in Lim N holds
x in A ) by Th22; ::_thesis: ( ( for N being convergent net of T st N is_eventually_in A holds
for x being Point of T st x in Lim N holds
x in A ) implies A is closed )
assume A1: for N being convergent net of T st N is_eventually_in A holds
for x being Point of T st x in Lim N holds
x in A ; ::_thesis: A is closed
 A = Cl A
proof
thus  A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A )
assume A2: x in Cl A ; ::_thesis: x in 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, Th22;
hence  x in A by A1; ::_thesis: verum
end;
hence  A is closed ; ::_thesis: verum
end;

theorem Th25: :: YELLOW19:25
for T being non empty TopSpace
for 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; ::_thesis: for 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 ) )
let A be Subset of T; ::_thesis: 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 ) )
let x be Point of T; ::_thesis: ( 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 ) )
hereby  ::_thesis: ( ex F being proper Filter of (BoolePoset ([#] T)) st
( A in F & x is_a_cluster_point_of F,T ) implies x in Cl A )
assume  x in Cl A ; ::_thesis: ex F being Subset of (BoolePoset ([#] T)) st
( A in F & x is_a_cluster_point_of F,T )
then consider N being net of T such that
A1: N is_eventually_in A and
A2: x is_a_cluster_point_of N by Th21;
set F = a_filter N;
take F = a_filter N; ::_thesis: ( A in F & x is_a_cluster_point_of F,T )
thus  A in F by A1; ::_thesis: x is_a_cluster_point_of F,T
thus  x is_a_cluster_point_of F,T by A2, Th11; ::_thesis: verum
end;
given F being proper Filter of (BoolePoset ([#] T)) such that A3: A in F and
A4: x is_a_cluster_point_of F,T ; ::_thesis: x in Cl A
reconsider F9 = F as proper Filter of (BoolePoset ([#] T)) ;
A5: a_filter (a_net F9) = F by Th14;
then A6: x is_a_cluster_point_of a_net F9 by A4, Th11;
 a_net F9 is_eventually_in A by A3, A5, Th10;
hence  x in Cl A by A6, Th21; ::_thesis: verum
end;

theorem Th26: :: YELLOW19:26
for T being non empty TopSpace
for 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; ::_thesis: for 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 ) )
let A be Subset of T; ::_thesis: 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 ) )
let x be Point of T; ::_thesis: ( 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 ) )
hereby  ::_thesis: ( ex F being ultra Filter of (BoolePoset ([#] T)) st
( A in F & x is_a_convergence_point_of F,T ) implies x in Cl A )
assume  x in Cl A ; ::_thesis: ex G being ultra Filter of (BoolePoset ([#] T)) st
( A in G & x is_a_convergence_point_of G,T )
then consider N being net of T such that
A1: N is_eventually_in A and
A2: x is_a_cluster_point_of N by Th21;
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: a_filter S c= G and
A5: G is ultra by WAYBEL_7:26;
reconsider G = G as ultra Filter of (BoolePoset ([#] T)) by A5;
take G = G; ::_thesis: ( A in G & x is_a_convergence_point_of G,T )
 S is_eventually_in A by A1, Th19;
then  A in a_filter S ;
hence  A in G by A4; ::_thesis: x is_a_convergence_point_of G,T
 x is_a_convergence_point_of a_filter S,T by A3, Th12;
hence  x is_a_convergence_point_of G,T by A4, Th20; ::_thesis: verum
end;
given F being ultra Filter of (BoolePoset ([#] T)) such that A6: A in F and
A7: x is_a_convergence_point_of F,T ; ::_thesis: x in Cl A
 x is_a_cluster_point_of F,T by A7, WAYBEL_7:27;
hence  x in Cl A by A6, Th25; ::_thesis: verum
end;

theorem :: YELLOW19:27
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds
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; ::_thesis: for A being Subset of T holds
( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_cluster_point_of F,T holds
x in A )
let A be Subset of T; ::_thesis: ( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_cluster_point_of F,T holds
x in A )
 ( A is closed iff Cl A = A ) by PRE_TOPC:22;
hence  ( A is closed implies for F being proper Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_cluster_point_of F,T holds
x in A ) by Th25; ::_thesis: ( ( for F being proper Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_cluster_point_of F,T holds
x in A ) implies A is closed )
assume A1: for F being proper Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_cluster_point_of F,T holds
x in A ; ::_thesis: A is closed
 A = Cl A
proof
thus  A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A )
assume A2: x in Cl A ; ::_thesis: x in 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, Th25;
hence  x in A by A1; ::_thesis: verum
end;
hence  A is closed ; ::_thesis: verum
end;

theorem :: YELLOW19:28
for T being non empty TopSpace
for A being Subset of T holds
( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
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; ::_thesis: for A being Subset of T holds
( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A )
let A be Subset of T; ::_thesis: ( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A )
 ( A is closed iff Cl A = A ) by PRE_TOPC:22;
hence  ( A is closed implies for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A ) by Th26; ::_thesis: ( ( for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A ) implies A is closed )
assume A1: for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds
for x being Point of T st x is_a_convergence_point_of F,T holds
x in A ; ::_thesis: A is closed
 A = Cl A
proof
thus  A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A )
assume A2: x in Cl A ; ::_thesis: x in 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, Th26;
hence  x in A by A1; ::_thesis: verum
end;
hence  A is closed ; ::_thesis: verum
end;

theorem Th29: :: YELLOW19:29
for T being non empty TopSpace
for 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; ::_thesis: for 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 )
let N be net of T; ::_thesis: 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 )
let s be Point of T; ::_thesis: ( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A )
hereby  ::_thesis: ( ( for A being Subset of T,N holds s in Cl A ) implies s is_a_cluster_point_of N )
assume A1: s is_a_cluster_point_of N ; ::_thesis: for A being Subset of T,N holds s in Cl A
let A be Subset of T,N; ::_thesis: s in Cl A
 N is_eventually_in A by Th8;
hence  s in Cl A by A1, Th21; ::_thesis: verum
end;
assume A2: for A being Subset of T,N holds s in Cl A ; ::_thesis: s is_a_cluster_point_of N
let V be a_neighborhood of s; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in V
let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of N st
( i <= b1 & N . b1 in V )
reconsider A = rng the mapping of (N | i) as Subset of T,N by Def2;
set x = the Element of A /\ (Int V);
A3: s in Int V by CONNSP_2:def_1;
 s in Cl A by A2;
then  A meets Int V by A3, PRE_TOPC:def_7;
then A4: A /\ (Int V) <> {} T by XBOOLE_0:def_7;
then A5: the Element of A /\ (Int V) in Int V by XBOOLE_0:def_4;
A6: Int V c= V by TOPS_1:16;
 the Element of A /\ (Int V) in A by A4, XBOOLE_0:def_4;
then consider j being set  such that
A7: j in dom the mapping of (N | i) and
A8: the Element of A /\ (Int V) = the mapping of (N | i) . j by FUNCT_1:def_3;
A9: the carrier of (N | i) =  {  l where l is Element of N : i <= l  }  by WAYBEL_9:12;
reconsider j = j as Element of (N | i) by A7;
 dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def_1;
then consider l being Element of N such that
A10: j = l and
A11: i <= l by A7, A9;
take  l ; ::_thesis: ( i <= l & N . l in V )
thus  i <= l by A11; ::_thesis: N . l in V
the Element of A /\ (Int V) = (N | i) . j by A8
.= N . l by A10, WAYBEL_9:16 ;
hence  N . l in V by A5, A6; ::_thesis: verum
end;

theorem :: YELLOW19:30
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; ::_thesis: for F being Subset-Family of T st F is closed holds
FinMeetCl F is closed
let F be Subset-Family of T; ::_thesis: ( F is closed implies FinMeetCl F is closed )
assume A1: F is closed ; ::_thesis: FinMeetCl F is closed
now__::_thesis:_for_P_being_Subset_of_T_st_P_in_FinMeetCl_F_holds_
P_is_closed
let P be Subset of T; ::_thesis: ( P in FinMeetCl F implies P is closed )
assume  P in FinMeetCl F ; ::_thesis: P is closed
then consider Y being Subset-Family of T such that
A2: Y c= F and
 Y is finite and
A3: P = Intersect Y by CANTOR_1:def_3;
A4: ( ( P = the carrier of T & the carrier of T = [#] T ) or P = meet Y ) by A3, SETFAM_1:def_9;
 for A being Subset of T st A in Y holds
A is closed by A1, A2, TOPS_2:def_2;
hence  P is closed by A4, PRE_TOPC:14; ::_thesis: verum
end;
hence  FinMeetCl F is closed by TOPS_2:def_2; ::_thesis: verum
end;

Lm1:  for T being non empty TopSpace st T is compact holds
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; ::_thesis: ( T is compact implies for N being net of T ex x being Point of T st x is_a_cluster_point_of N )
assume A1: T is compact ; ::_thesis: for N being net of T ex x being Point of T st x is_a_cluster_point_of N
let N be net of T; ::_thesis: ex x being Point of T st x is_a_cluster_point_of N
set F =  {  (Cl A) where A is Subset of T,N : verum  }  ;
  {  (Cl A) where A is Subset of T,N : verum  }  c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (Cl A) where A is Subset of T,N : verum  }  or x in bool the carrier of T )
assume  x in  {  (Cl A) where A is Subset of T,N : verum  }  ; ::_thesis: x in bool the carrier of T
then  ex A being Subset of T,N st x = Cl A ;
hence  x in bool the carrier of T ; ::_thesis: verum
end;
then reconsider F =  {  (Cl A) where A is Subset of T,N : verum  }  as Subset-Family of T ;
set x = the Element of meet F;
A2: F is centered
proof
defpred S1[ set , set ] means  ex A being Subset of T,N ex i being Element of N st
( $1 = Cl A & $2 = i & A = rng the mapping of (N | i) );
set A0 = the Subset of T,N;
 Cl the Subset of T,N in F ;
hence  F <> {} ; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds
( b1 = {} or not b1 c= F or not b1 is finite or not meet b1 = {} )
let G be set ; ::_thesis: ( G = {} or not G c= F or not G is finite or not meet G = {} )
assume that
A3: G <> {} and
A4: G c= F and
A5: G is finite ; ::_thesis: not meet G = {}
A6: now__::_thesis:_for_x_being_set_st_x_in_G_holds_
ex_y_being_set_st_
(_y_in_the_carrier_of_N_&_S1[x,y]_)
let x be set ; ::_thesis: ( x in G implies ex y being set st
( y in the carrier of N & S1[x,y] ) )
assume  x in G ; ::_thesis: ex y being set st
( y in the carrier of N & S1[x,y] )
then  x in F by A4;
then consider A being Subset of T,N such that
A7: x = Cl A ;
consider i being Element of N such that
A8: A = rng the mapping of (N | i) by Def2;
reconsider y = i as set ;
take y = y; ::_thesis: ( y in the carrier of N & S1[x,y] )
thus  y in the carrier of N ; ::_thesis: S1[x,y]
thus  S1[x,y] by A7, A8; ::_thesis: verum
end;
consider f being Function such that
A9: ( dom f = G & rng f c= the carrier of N ) and
A10: for x being set st x in G holds
S1[x,f . x] from FUNCT_1:sch_5(A6);
reconsider B = rng f as finite Subset of N by A5, A9, FINSET_1:8;
 [#] N is directed by WAYBEL_0:def_6;
then consider j being Element of N such that
 j in [#] N and
A11: j is_>=_than B by WAYBEL_0:1;
now__::_thesis:_for_X_being_set_st_X_in_G_holds_
N_._j_in_X
let X be set ; ::_thesis: ( X in G implies N . j in X )
assume A12: X in G ; ::_thesis: N . j in X
then consider A being Subset of T,N, i being Element of N such that
A13: X = Cl A and
A14: f . X = i and
A15: A = rng the mapping of (N | i) by A10;
A16: A c= X by A13, PRE_TOPC:18;
A17: the mapping of (N | i) = the mapping of N | the carrier of (N | i) by WAYBEL_9:def_7;
 i in B by A9, A12, A14, FUNCT_1:def_3;
then  i <= j by A11, LATTICE3:def_9;
then  j in the carrier of (N | i) by WAYBEL_9:def_7;
then A18: j in dom the mapping of (N | i) by FUNCT_2:def_1;
then  the mapping of (N | i) . j in A by A15, FUNCT_1:def_3;
then  N . j in A by A18, A17, FUNCT_1:47;
hence  N . j in X by A16; ::_thesis: verum
end;
hence  not meet G = {} by A3, SETFAM_1:def_1; ::_thesis: verum
end;
 F is closed
proof
let S be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not S in F or S is closed )
assume  S in F ; ::_thesis: S is closed
then  ex A being Subset of T,N st S = Cl A ;
hence  S is closed ; ::_thesis: verum
end;
then A19: meet F <> {} by A1, A2, COMPTS_1:4;
then  the Element of meet F in meet F ;
then reconsider x = the Element of meet F as Point of T ;
take  x ; ::_thesis: x is_a_cluster_point_of N
now__::_thesis:_for_A_being_Subset_of_T,N_holds_x_in_Cl_A
let A be Subset of T,N; ::_thesis: x in Cl A
 Cl A in F ;
hence  x in Cl A by A19, SETFAM_1:def_1; ::_thesis: verum
end;
hence  x is_a_cluster_point_of N by Th29; ::_thesis: verum
end;

Lm2:  for T being non empty TopSpace st ( for N being net of T st N in NetUniv T holds
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; ::_thesis: ( ( for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N ) implies T is compact )
assume A1: for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N ; ::_thesis: T is compact
now__::_thesis:_for_F_being_Subset-Family_of_T_st_F_is_centered_&_F_is_closed_holds_
meet_F_<>_{}
set X = the carrier of T;
defpred S1[ set , set ] means $2 in $1;
let F be Subset-Family of T; ::_thesis: ( F is centered & F is closed implies meet F <> {} )
assume that
A2: F is centered and
A3: F is closed ; ::_thesis: meet F <> {}
set G = FinMeetCl F;
A4: now__::_thesis:_for_x_being_set_st_x_in_FinMeetCl_F_holds_
ex_y_being_set_st_
(_y_in_the_carrier_of_T_&_S1[x,y]_)
let x be set ; ::_thesis: ( x in FinMeetCl F implies ex y being set st
( y in the carrier of T & S1[x,y] ) )
set y = the Element of x;
assume  x in FinMeetCl F ; ::_thesis: ex y being set st
( y in the carrier of T & S1[x,y] )
then consider Y being Subset-Family of T such that
A5: Y c= F and
A6: Y is finite and
A7: x = Intersect Y by CANTOR_1:def_3;
 ( Y = {} or Y <> {} ) ;
then  ( x = the carrier of T or ( x = meet Y & meet Y <> {} ) ) by A2, A5, A6, A7, FINSET_1:def_3, SETFAM_1:def_9;
then  the Element of x in x ;
hence  ex y being set st
( y in the carrier of T & S1[x,y] ) by A7; ::_thesis: verum
end;
consider f being Function such that
A8: ( dom f = FinMeetCl F & rng f c= the carrier of T ) and
A9: for a being set st a in FinMeetCl F holds
S1[a,f . a] from FUNCT_1:sch_5(A4);
A10: F c= FinMeetCl F by CANTOR_1:4;
A11: F <> {} by A2, FINSET_1:def_3;
then reconsider G = FinMeetCl F as non empty Subset-Family of T by A10;
set R = (InclPoset G) opp ;
A12: InclPoset G = RelStr(# G,(RelIncl G) #) by YELLOW_1:def_1;
then A13: the carrier of ((InclPoset G) opp) = G by YELLOW_6:3;
 (InclPoset G) opp is directed
proof
let x, y be Element of ((InclPoset G) opp); :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] ((InclPoset G) opp) or not y in [#] ((InclPoset G) opp) or ex b1 being Element of the carrier of ((InclPoset G) opp) st
( b1 in [#] ((InclPoset G) opp) & x <= b1 & y <= b1 ) )
assume that
 x in [#] ((InclPoset G) opp) and
 y in [#] ((InclPoset G) opp) ; ::_thesis: ex b1 being Element of the carrier of ((InclPoset G) opp) st
( b1 in [#] ((InclPoset G) opp) & x <= b1 & y <= b1 )
A14: ~ x = x by LATTICE3:def_7;
 y in G by A13;
then consider Y being Subset-Family of T such that
A15: Y c= F and
A16: Y is finite and
A17: y = Intersect Y by CANTOR_1:def_3;
 x in G by A13;
then consider X being Subset-Family of T such that
A18: X c= F and
A19: X is finite and
A20: x = Intersect X by CANTOR_1:def_3;
set z = Intersect (X \/ Y);
 X \/ Y c= F by A18, A15, XBOOLE_1:8;
then reconsider z = Intersect (X \/ Y) as Element of ((InclPoset G) opp) by A13, A19, A16, CANTOR_1:def_3;
A21: ~ z = z by LATTICE3:def_7;
take  z ; ::_thesis: ( z in [#] ((InclPoset G) opp) & x <= z & y <= z )
thus  z in [#] ((InclPoset G) opp) ; ::_thesis: ( x <= z & y <= z )
A22: ~ y = y by LATTICE3:def_7;
 z c= y by A17, SETFAM_1:44, XBOOLE_1:7;
then A23: ~ z <= ~ y by A22, A21, YELLOW_1:3;
 z c= x by A20, SETFAM_1:44, XBOOLE_1:7;
then  ~ z <= ~ x by A14, A21, YELLOW_1:3;
hence  ( x <= z & y <= z ) by A23, YELLOW_7:1; ::_thesis: verum
end;
then reconsider R = (InclPoset G) opp as non empty transitive directed RelStr ;
reconsider f = f as Function of the carrier of R, the carrier of T by A8, A13, FUNCT_2:2;
set N = R *' f;
A24: RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by WAYBEL32:def_3;
A25: the_universe_of the carrier of T = Tarski-Class (the_transitive-closure_of the carrier of T) by YELLOW_6:def_1;
 the carrier of T c= the_transitive-closure_of the carrier of T by CLASSES1:52;
then  the carrier of T in Tarski-Class (the_transitive-closure_of the carrier of T) by CLASSES1:2, CLASSES1:3;
then  bool the carrier of T in Tarski-Class (the_transitive-closure_of the carrier of T) by CLASSES1:4;
then  G in Tarski-Class (the_transitive-closure_of the carrier of T) by CLASSES1:3;
then  R *' f in NetUniv T by A13, A24, A25, YELLOW_6:def_11;
then consider x being Point of T such that
A26: x is_a_cluster_point_of R *' f by A1;
A27: the mapping of (R *' f) = f by WAYBEL32:def_3;
now__::_thesis:_for_X_being_set_st_X_in_F_holds_
x_in_X
let X be set ; ::_thesis: ( X in F implies x in X )
assume A28: X in F ; ::_thesis: x in X
then reconsider A = X as Subset of T ;
reconsider a = X as Element of (R *' f) by A10, A12, A24, A28, YELLOW_6:3;
A29: now__::_thesis:_for_V_being_Subset_of_T_st_V_is_open_&_x_in_V_holds_
A_meets_V
let V be Subset of T; ::_thesis: ( V is open & x in V implies A meets V )
assume that
A30: V is open and
A31: x in V ; ::_thesis: A meets V
 Int V = V by A30, TOPS_1:23;
then  V is a_neighborhood of x by A31, CONNSP_2:def_1;
then  R *' f is_often_in V by A26, WAYBEL_9:def_9;
then consider b being Element of (R *' f) such that
A32: a <= b and
A33: (R *' f) . b in V by WAYBEL_0:def_12;
reconsider a9 = a, b9 = b as Element of ((InclPoset G) opp) by A24;
 a9 <= b9 by A24, A32, YELLOW_0:1;
then A34: ~ a9 >= ~ b9 by YELLOW_7:1;
A35: ~ b9 = b by LATTICE3:def_7;
 ~ a9 = A by LATTICE3:def_7;
then A36: b c= A by A34, A35, YELLOW_1:3;
 (R *' f) . b in b by A9, A12, A27, A35;
hence  A meets V by A33, A36, XBOOLE_0:3; ::_thesis: verum
end;
 A is closed by A3, A28, TOPS_2:def_2;
then  Cl A = A by PRE_TOPC:22;
hence  x in X by A29, PRE_TOPC:def_7; ::_thesis: verum
end;
hence  meet F <> {} by A11, SETFAM_1:def_1; ::_thesis: verum
end;
hence  T is compact by COMPTS_1:4; ::_thesis: verum
end;

theorem Th31: :: YELLOW19:31
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; ::_thesis: ( 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 )
set X = the carrier of T;
hereby  ::_thesis: ( ( for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ) implies T is compact )
assume A1: T is compact ; ::_thesis: for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T
let F be ultra Filter of (BoolePoset ([#] T)); ::_thesis: ex x being Point of T st x is_a_convergence_point_of F,T
set G =  {  (Cl A) where A is Subset of T : A in F  }  ;
  {  (Cl A) where A is Subset of T : A in F  }  c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (Cl A) where A is Subset of T : A in F  }  or x in bool the carrier of T )
assume  x in  {  (Cl A) where A is Subset of T : A in F  }  ; ::_thesis: x in bool the carrier of T
then  ex A being Subset of T st
( x = Cl A & A in F ) ;
hence  x in bool the carrier of T ; ::_thesis: verum
end;
then reconsider G =  {  (Cl A) where A is Subset of T : A in F  }  as Subset-Family of T ;
A2: G is centered
proof
set A0 = the Element of F;
reconsider A0 = the Element of F as Subset of T by WAYBEL_7:2;
 Cl A0 in G ;
hence  G <> {} ; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds
( b1 = {} or not b1 c= G or not b1 is finite or not meet b1 = {} )
let H be set ; ::_thesis: ( H = {} or not H c= G or not H is finite or not meet H = {} )
assume that
A3: H <> {} and
A4: H c= G and
A5: H is finite ; ::_thesis: not meet H = {}
reconsider H1 = H as finite Subset-Family of the carrier of T by A4, A5, XBOOLE_1:1;
 H1 c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1 or x in F )
assume  x in H1 ; ::_thesis: x in F
then  x in G by A4;
then consider A being Subset of T such that
A6: x = Cl A and
A7: A in F ;
 A c= Cl A by PRE_TOPC:18;
hence  x in F by A6, A7, WAYBEL_7:7; ::_thesis: verum
end;
then  Intersect H1 in F by WAYBEL_7:11;
then  Intersect H1 <> {} by Th1;
hence  not meet H = {} by A3, SETFAM_1:def_9; ::_thesis: verum
end;
set x = the Element of meet G;
 G is closed
proof
let A be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not A in G or A is closed )
assume  A in G ; ::_thesis: A is closed
then  ex B being Subset of T st
( A = Cl B & B in F ) ;
hence  A is closed ; ::_thesis: verum
end;
then A8: meet G <> {} by A1, A2, COMPTS_1:4;
then  the Element of meet G in meet G ;
then reconsider x = the Element of meet G as Point of T ;
take x = x; ::_thesis: x is_a_convergence_point_of F,T
thus  x is_a_convergence_point_of F,T ::_thesis: verum
proof
let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not x in A or A in F )
assume that
A9: A is open and
A10: x in A ; ::_thesis: A in F
set B = A ` ;
A11: now__::_thesis:_not_A_`_in_F
assume  A ` in F ; ::_thesis: contradiction
then  Cl (A `) in G ;
then A12: A ` in G by A9, PRE_TOPC:22;
 not x in A ` by A10, XBOOLE_0:def_5;
hence  contradiction by A8, A12, SETFAM_1:def_1; ::_thesis: verum
end;
 F is prime by WAYBEL_7:22;
hence  A in F by A11, WAYBEL_7:21; ::_thesis: verum
end;
end;
assume A13: for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ; ::_thesis: T is compact
now__::_thesis:_for_F_being_Subset-Family_of_T_st_F_is_centered_&_F_is_closed_holds_
meet_F_<>_{}
set L = BoolePoset the carrier of T;
let F be Subset-Family of T; ::_thesis: ( F is centered & F is closed implies meet F <> {} )
assume A14: ( F is centered & F is closed ) ; ::_thesis: meet F <> {}
reconsider Y = F as Subset of (BoolePoset the carrier of T) by WAYBEL_7:2;
set G = uparrow (fininfs Y);
now__::_thesis:_not_Bottom_(BoolePoset_the_carrier_of_T)_in_uparrow_(fininfs_Y)
assume  Bottom (BoolePoset the carrier of T) in uparrow (fininfs Y) ; ::_thesis: contradiction
then consider x being Element of (BoolePoset the carrier of T) such that
A15: x <= Bottom (BoolePoset the carrier of T) and
A16: x in fininfs Y by WAYBEL_0:def_16;
A17: Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;
consider Z being finite Subset of Y such that
A18: x = "/\" (Z,(BoolePoset the carrier of T)) and
 ex_inf_of Z, BoolePoset the carrier of T by A16;
reconsider Z = Z as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;
A19: x = Bottom (BoolePoset the carrier of T) by A15, YELLOW_5:19;
then  x <> Top (BoolePoset the carrier of T) by WAYBEL_7:3;
then A20: Z <> {} by A18, YELLOW_0:def_12;
then  meet Z <> {} by A14, FINSET_1:def_3;
hence  contradiction by A17, A18, A19, A20, YELLOW_1:20; ::_thesis: verum
end;
then  uparrow (fininfs Y) is proper by WAYBEL_7:4;
then consider UF being Filter of (BoolePoset the carrier of T) such that
A21: uparrow (fininfs Y) c= UF and
A22: UF is ultra by WAYBEL_7:26;
consider x being Point of T such that
A23: x is_a_convergence_point_of UF,T by A13, A22;
 F c= uparrow (fininfs Y) by WAYBEL_0:62;
then A24: F c= UF by A21, XBOOLE_1:1;
A25: now__::_thesis:_for_A_being_set_st_A_in_F_holds_
x_in_A
let A be set ; ::_thesis: ( A in F implies x in A )
assume A26: A in F ; ::_thesis: x in A
then reconsider B = A as Subset of T ;
A27: now__::_thesis:_for_C_being_Subset_of_T_st_C_is_open_&_x_in_C_holds_
A_meets_C
let C be Subset of T; ::_thesis: ( C is open & x in C implies A meets C )
assume that
A28: C is open and
A29: x in C ; ::_thesis: A meets C
A30: C in UF by A23, A28, A29, WAYBEL_7:def_5;
 A in UF by A24, A26;
then reconsider c = C, a = A as Element of (BoolePoset the carrier of T) by A30;
 a "/\" c in UF by A24, A26, A30, WAYBEL_0:41;
then  a "/\" c <> {} by A22, Th1;
then  A /\ C <> {} by YELLOW_1:17;
hence  A meets C by XBOOLE_0:def_7; ::_thesis: verum
end;
 B is closed by A14, A26, TOPS_2:def_2;
then  Cl B = B by PRE_TOPC:22;
hence  x in A by A27, PRE_TOPC:24; ::_thesis: verum
end;
 F <> {} by A14, FINSET_1:def_3;
hence  meet F <> {} by A25, SETFAM_1:def_1; ::_thesis: verum
end;
hence  T is compact by COMPTS_1:4; ::_thesis: verum
end;

theorem :: YELLOW19:32
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; ::_thesis: ( 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 )
hereby  ::_thesis: ( ( for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T ) implies T is compact )
assume A1: T is compact ; ::_thesis: for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T
let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: ex x being Point of T st x is_a_cluster_point_of F,T
reconsider G = F as proper Filter of (BoolePoset ([#] T)) ;
consider x being Point of T such that
A2: x is_a_cluster_point_of a_net G by A1, Lm1;
take x = x; ::_thesis: x is_a_cluster_point_of F,T
thus  x is_a_cluster_point_of F,T by A2, Th16; ::_thesis: verum
end;
assume A3: for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T ; ::_thesis: T is compact
now__::_thesis:_for_N_being_net_of_T_st_N_in_NetUniv_T_holds_
ex_x_being_Point_of_T_st_x_is_a_cluster_point_of_N
let N be net of T; ::_thesis: ( N in NetUniv T implies ex x being Point of T st x is_a_cluster_point_of N )
assume  N in NetUniv T ; ::_thesis: ex x being Point of T st x is_a_cluster_point_of N
reconsider F = a_filter N as proper Filter of (BoolePoset the carrier of T) ;
consider x being Point of T such that
A4: x is_a_cluster_point_of F,T by A3;
take x = x; ::_thesis: x is_a_cluster_point_of N
thus  x is_a_cluster_point_of N by A4, Th11; ::_thesis: verum
end;
hence  T is compact by Lm2; ::_thesis: verum
end;

theorem Th33: :: YELLOW19:33
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; ::_thesis: ( T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N )
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; ::_thesis: ( ( for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) implies T is compact )
assume  for N being net of T ex x being Point of T st x is_a_cluster_point_of N ; ::_thesis: T is compact
then  for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N ;
hence  T is compact by Lm2; ::_thesis: verum
end;

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

registration
let L be non empty 1-sorted ;
let N be transitive NetStr over L;
cluster full  ->  transitive full for SubNetStr of N;
coherence
 for b1 being full SubNetStr of N holds b1 is transitive
proof
let S be full SubNetStr of N; ::_thesis: S is transitive
 S is full SubRelStr of N by YELLOW_6:def_7;
hence  S is transitive ; ::_thesis: verum
end;
end;

registration
let L be non empty 1-sorted ;
let N be non empty directed NetStr over L;
cluster non empty strict directed full for SubNetStr of N;
existence
 ex b1 being SubNetStr of N st
( b1 is strict & not b1 is empty & b1 is directed & b1 is full )
proof
set S = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #);
A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N, the InternalRel of N #) ;
 N is full SubRelStr of N by YELLOW_6:6;
then A2: NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is full SubRelStr of N by A1, WAYBEL21:12;
 N is SubNetStr of N by YELLOW_6:8;
then  the mapping of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = the mapping of N | the carrier of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) by YELLOW_6:def_6;
then reconsider S = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) as non empty strict full SubNetStr of N by A2, YELLOW_6:def_6, YELLOW_6:def_7;
 [#] N is directed by WAYBEL_0:def_6;
then  [#] S is directed by A1, WAYBEL_0:3;
then  S is directed by WAYBEL_0:def_6;
hence  ex b1 being SubNetStr of N st
( b1 is strict & not b1 is empty & b1 is directed & b1 is full ) ; ::_thesis: verum
end;
end;

theorem :: YELLOW19:35
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; ::_thesis: ( T is compact iff for N being net of T ex S being subnet of N st S is convergent )
hereby  ::_thesis: ( ( for N being net of T ex S being subnet of N st S is convergent ) implies T is compact )
assume A1: T is compact ; ::_thesis: for N being net of T ex S being subnet of N st S is convergent
let N be net of T; ::_thesis: ex S being subnet of N st S is convergent
consider x being Point of T such that
A2: x is_a_cluster_point_of N by A1, Th33;
consider S being subnet of N such that
A3: x in Lim S by A2, WAYBEL_9:32;
take S = S; ::_thesis: S is convergent
thus  S is convergent by A3, YELLOW_6:def_16; ::_thesis: verum
end;
assume A4: for N being net of T ex S being subnet of N st S is convergent ; ::_thesis: T is compact
now__::_thesis:_for_N_being_net_of_T_ex_x_being_Point_of_T_st_x_is_a_cluster_point_of_N
let N be net of T; ::_thesis: ex x being Point of T st x is_a_cluster_point_of N
consider S being subnet of N such that
A5: S is convergent by A4;
set x = the Element of Lim S;
A6: Lim S <> {} by A5, YELLOW_6:def_16;
then  the Element of Lim S in Lim S ;
then reconsider x = the Element of Lim S as Point of T ;
take x = x; ::_thesis: x is_a_cluster_point_of N
thus  x is_a_cluster_point_of N by A6, WAYBEL_9:29, WAYBEL_9:31; ::_thesis: verum
end;
hence  T is compact by Th33; ::_thesis: verum
end;

definition
let S be non empty 1-sorted ;
let N be non empty NetStr over S;
attrN is Cauchy  means :: YELLOW19:def 5
 for A being Subset of S holds
( N is_eventually_in A or N is_eventually_in A ` );
end;

:: deftheorem  defines Cauchy YELLOW19:def_5_:_
 for S being non empty 1-sorted
for N being non empty NetStr over S holds
( N is Cauchy iff for A being Subset of S holds
( N is_eventually_in A or N is_eventually_in A ` ) );

registration
let S be non empty 1-sorted ;
let F be ultra Filter of (BoolePoset ([#] S));
cluster a_net F ->  non empty strict Cauchy ;
coherence
 a_net F is Cauchy
proof
let A be Subset of S; :: according to YELLOW19:def_5 ::_thesis: ( a_net F is_eventually_in A or a_net F is_eventually_in A ` )
 F is prime by WAYBEL_7:22;
then A1: ( ( ( A is empty or not A is empty ) & ( A ` is empty or not A ` is empty ) & A in F ) or A ` in F ) by WAYBEL_7:21;
 ({} S) ` = [#] S ;
then  ( A ` = {} S implies A = [#] S ) ;
hence  ( a_net F is_eventually_in A or a_net F is_eventually_in A ` ) by A1, Th15, YELLOW_6:20; ::_thesis: verum
end;
end;

theorem :: YELLOW19:36
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; ::_thesis: ( T is compact iff for N being net of T st N is Cauchy holds
N is convergent )
thus  ( T is compact implies for N being net of T st N is Cauchy holds
N is convergent ) ::_thesis: ( ( for N being net of T st N is Cauchy holds
N is convergent ) implies T is compact )
proof
assume A1: T is compact ; ::_thesis: for N being net of T st N is Cauchy holds
N is convergent
let N be net of T; ::_thesis: ( N is Cauchy implies N is convergent )
assume A2: for A being Subset of T holds
( N is_eventually_in A or N is_eventually_in A ` ) ; :: according to YELLOW19:def_5 ::_thesis: N is convergent
consider x being Point of T such that
A3: x is_a_cluster_point_of N by A1, Lm1;
now__::_thesis:_for_V_being_a_neighborhood_of_x_holds_N_is_eventually_in_V
let V be a_neighborhood of x; ::_thesis: N is_eventually_in V
assume  not N is_eventually_in V ; ::_thesis: contradiction
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 and
A6: N . j in V by WAYBEL_0:def_12;
 N . j in V ` by A4, A5;
hence  contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then  x in Lim N by YELLOW_6:def_15;
hence  N is convergent by YELLOW_6:def_16; ::_thesis: verum
end;
assume A7: for N being net of T st N is Cauchy holds
N is convergent ; ::_thesis: T is compact
now__::_thesis:_for_F_being_ultra_Filter_of_(BoolePoset_([#]_T))_ex_x_being_Point_of_T_st_x_is_a_convergence_point_of_F,T
let F be ultra Filter of (BoolePoset ([#] T)); ::_thesis: ex x being Point of T st x is_a_convergence_point_of F,T
set x = the Element of Lim (a_net F);
 a_net F is convergent by A7;
then A8: Lim (a_net F) <> {} by YELLOW_6:def_16;
then  the Element of Lim (a_net F) in Lim (a_net F) ;
then reconsider x = the Element of Lim (a_net F) as Point of T ;
take x = x; ::_thesis: x is_a_convergence_point_of F,T
thus  x is_a_convergence_point_of F,T by A8, Th17; ::_thesis: verum
end;
hence  T is compact by Th31; ::_thesis: verum
end;