defpred S1[ 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 ;
then A in V by A7, A9;
hence x in union V by ; :: 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 ;
A11: now :: thesis: for A being object st A in W holds
ex B being object st
( B in F & S1[A,B] )
let A be object ; :: thesis: ( A in W implies ex B being object st
( B in F & S1[A,B] ) )

assume A in W ; :: thesis: ex B being object st
( B in F & S1[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 & S1[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
S1[A,f . A] ) ) from rng f is finite by ;
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 ;
set a = the Element of x9 "/\" z;
x9 "/\" z in F by ;
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 ;
then consider A being set such that
A17: the Element of x9 "/\" z in A and
A18: A in W by ;
A19: the Element of x9 "/\" z in z by ;
A20: f . A in rng f by ;
then f . A in F by A12;
then reconsider b = f . A as Element of (BoolePoset the carrier of T) ;
z <= b by ;
then A21: z c= b by YELLOW_1:2;
S1[A,f . A] by ;
then A misses b ;
hence contradiction by A19, A17, A21, XBOOLE_0:3; :: thesis: verum