defpred S₁[ object , object ] means ex A, B being set st
( A = $1 & B = $2 & A misses B );
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 A2: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def 1;
( 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) #) ) by YELLOW_1:def 1;
then reconsider x9 = x as Element of (BoolePoset the carrier of T) by A2;
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
A3: x in F and
A4: 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 object ; :: 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 ;
A5: y c= union V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in y or x in union V )
assume A6: 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 A4, A6;
then consider A being Subset of T such that
A7: A is open and
A8: x in A and
A9: ex B being set st
( B in F & A misses B ) ;
A meets y by A6, A8, XBOOLE_0:3;
then A in V by A7, A9;
hence x in union V by A8, TARSKI:def 4; :: thesis: verum

end;

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;

then consider W being finite Subset of V such that
A10: x c= union W by A1, A5, WAYBEL_3:34;

A11: now :: thesis: for A being object st A in W holds
ex B being object st
( B in F & S₁[A,B] )

let A be object ; :: thesis: ( A in W implies ex B being object st
( B in F & S₁[A,B] ) )
assume A in W ; :: thesis: ex B being object 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 object st
( B in F & S₁[A,B] ) ; :: thesis: verum

end;

consider f being Function such that
A12: ( dom f = W & rng f c= F & ( for A being object st A in W holds
S₁[A,f . A] ) ) from FUNCT_1:sch 6(A11);
rng f is finite by A12, FINSET_1:8;
then consider z being Element of (BoolePoset the carrier of T) such that
A13: z in F and
A14: z is_<=_than rng f by A12, WAYBEL_0:2;
set a = the Element of x9 "/\" z;
x9 "/\" z in F by A3, A13, WAYBEL_0:41;
then x9 "/\" z <> Bottom (BoolePoset the carrier of T) by Th4;
then x9 "/\" z <> {} by YELLOW_1:18;
then A15: the Element of x9 "/\" z in x9 "/\" z ;
A16: x9 "/\" z c= x9 /\ z by YELLOW_1:17;
then the Element of x9 "/\" z in x by A15, XBOOLE_0:def 4;
then consider A being set such that
A17: the Element of x9 "/\" z in A and
A18: A in W by A10, TARSKI:def 4;
A19: the Element of x9 "/\" z in z by A15, A16, XBOOLE_0:def 4;
A20: f . A in rng f by A12, A18, FUNCT_1:def 3;
then f . A in F by A12;
then reconsider b = f . A as Element of (BoolePoset the carrier of T) ;
z <= b by A14, A20, LATTICE3:def 8;
then A21: z c= b by YELLOW_1:2;
S₁[A,f . A] by A12, A18;
then A misses b ;
hence contradiction by A19, A17, A21, XBOOLE_0:3; :: thesis: verum