defpred S1[ object , object ] means ex A, B being set st
( A = $1 & B = $2 & A misses B );
let T be non empty TopSpace; 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); ( 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
; 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); ( 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
; 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
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
V is open
then consider W being finite Subset of V such that
A10:
x c= union W
by A1, A5, WAYBEL_3:34;
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 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;
S1[A,f . A]
by A12, A18;
then
A misses b
;
hence
contradiction
by A19, A17, A21, XBOOLE_0:3; verum