defpred S_{1}[ 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

( B in F & A misses B ) ) } as Subset-Family of T ;

reconsider V = V as Subset-Family of T ;

A5: y c= union V

A10: x c= union W by A1, A5, WAYBEL_3:34;

A12: ( dom f = W & rng f c= F & ( for A being object st A in W holds

S_{1}[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_{1}[A,f . A]
by A12, A18;

then A misses b ;

hence contradiction by A19, A17, A21, XBOOLE_0:3; :: thesis: verum

( 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

then reconsider V = { A where A is Subset of T : ( A is open & A meets y & ex B being set st
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;( 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

( 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

V is open
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;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

proof

then consider W being finite Subset of V such that
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;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

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_{1}[A,B] )

consider f being Function such that ex B being object st

( B in F & S

let A be object ; :: thesis: ( A in W implies ex B being object st

( B in F & S_{1}[A,B] ) )

assume A in W ; :: thesis: ex B being object st

( B in F & S_{1}[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_{1}[A,B] )
; :: thesis: verum

end;( B in F & S

assume A in W ; :: thesis: ex B being object st

( B in F & S

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

A12: ( dom f = W & rng f c= F & ( for A being object st A in W holds

S

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

then A misses b ;

hence contradiction by A19, A17, A21, XBOOLE_0:3; :: thesis: verum