let T be non empty TopSpace; :: thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds
for F being proper Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T )
set L = InclPoset the topology of T;
set B = BoolePoset the carrier of T;
let x, y be Element of (InclPoset the topology of T); :: thesis: ( x << y implies for F being proper Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T ) )
assume A1: x << y ; :: thesis: for F being proper Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T )
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then ( x in the carrier of (InclPoset the topology of T) & InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) & BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) ) by YELLOW_1:def 1;
then reconsider x' = x as Element of (BoolePoset the carrier of T) ;
let F be proper Filter of (BoolePoset the carrier of T); :: thesis: ( x in F implies ex p being Element of T st
( p in y & p is_a_cluster_point_of F,T ) )
assume that
A2: x in F and
A3: for x being Element of T st x in y holds
not x is_a_cluster_point_of F,T ; :: thesis: contradiction
set V = { A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } ;
{ A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } c= bool the carrier of T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } or a in bool the carrier of T )
assume a in { A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } ; :: thesis: a in bool the carrier of T
then ex C being Subset of T st
( a = C & C is open & C meets y & ex B being set st
( B in F & C misses B ) ) ;
hence a in bool the carrier of T ; :: thesis: verum

end;

then reconsider V = { A where A is Subset of T : ( A is open & A meets y & ex B being set st
( B in F & A misses B ) ) } as Subset-Family of T ;
reconsider V = V as Subset-Family of T ;
A4: V is open

proof

let a be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not a in V or a is open )
assume a in V ; :: thesis: a is open
then ex C being Subset of T st
( a = C & C is open & C meets y & ex B being set st
( B in F & C misses B ) ) ;
hence a is open ; :: thesis: verum

end;

y c= union V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in y or x in union V )
assume A5: x in y ; :: thesis: x in union V
InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;
then y in the topology of T ;
then not x is_a_cluster_point_of F,T by A3, A5;
then consider A being Subset of T such that
A6: ( A is open & x in A & ex B being set st
( B in F & A misses B ) ) by Def4;
A meets y by A5, A6, XBOOLE_0:3;
then A in V by A6;
hence x in union V by A6, TARSKI:def 4; :: thesis: verum

end;

then consider W being finite Subset of V such that
A7: x c= union W by A1, A4, WAYBEL_3:34;
defpred S₁[ set , set ] means $1 misses $2;

A8: now

let A be set ; :: thesis: ( A in W implies ex B being set st
( B in F & S₁[A,B] ) )
assume A in W ; :: thesis: ex B being set st
( B in F & S₁[A,B] )
then A in V ;
then ex C being Subset of T st
( A = C & C is open & C meets y & ex B being set st
( B in F & C misses B ) ) ;
hence ex B being set st
( B in F & S₁[A,B] ) ; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = W & rng f c= F & ( for A being set st A in W holds
S₁[A,f . A] ) ) from WELLORD2:sch 1(A8);
rng f is finite by A9, FINSET_1:26;
then consider z being Element of (BoolePoset the carrier of T) such that
A10: ( z in F & z is_<=_than rng f ) by A9, WAYBEL_0:2;
consider a being Element of x' "/\" z;
x' "/\" z in F by A2, A10, WAYBEL_0:41;
then x' "/\" z <> Bottom (BoolePoset the carrier of T) by Th8;
then x' "/\" z <> {} by YELLOW_1:18;
then ( a in x' "/\" z & x' "/\" z c= x' /\ z ) by YELLOW_1:17;
then A11: ( a in x & a in z ) by XBOOLE_0:def 4;
then consider A being set such that
A12: ( a in A & A in W ) by A7, TARSKI:def 4;
A13: f . A in rng f by A9, A12, FUNCT_1:def 5;
then f . A in F by A9;
then reconsider b = f . A as Element of (BoolePoset the carrier of T) ;
( A misses b & z <= b ) by A9, A10, A12, A13, LATTICE3:def 8;
then ( not a in b & z c= b ) by A12, XBOOLE_0:3, YELLOW_1:2;
hence contradiction by A11; :: thesis: verum