let T be non empty TopSpace; :: thesis: for x, y being Element of (InclPoset the topology of T) st x c= y & ( for F being ultra 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_convergence_point_of F,T ) ) holds

x << y

set B = BoolePoset the carrier of T;

let x, y be Element of (InclPoset the topology of T); :: thesis: ( x c= y & ( for F being ultra 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_convergence_point_of F,T ) ) implies x << y )

assume that

A1: x c= y and

A2: for F being ultra 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_convergence_point_of F,T ) ; :: thesis: x << y

InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;

then x in the topology of T ;

then reconsider X = x as Subset of T ;

reconsider X = X as Subset of T ;

assume not x << y ; :: thesis: contradiction

then consider F being Subset-Family of T such that

A3: F is open and

A4: y c= union F and

A5: for G being finite Subset of F holds not x c= union G by WAYBEL_3:35;

set xF = { (x \ z) where z is Subset of T : z in F } ;

set z = the Element of F;

BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;

then A9: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def 1;

{ (x \ z) where z is Subset of T : z in F } c= the carrier of (BoolePoset the carrier of T)

set FF = uparrow (fininfs xF);

then consider GG being Filter of (BoolePoset the carrier of T) such that

A22: uparrow (fininfs xF) c= GG and

A23: GG is ultra by Th26;

reconsider z = the Element of F as Subset of T by A8;

A24: xF c= uparrow (fininfs xF) by WAYBEL_0:62;

x \ z in xF by A6;

then A25: x \ z in uparrow (fininfs xF) by A24;

x \ z c= X ;

then x in GG by A22, A25, Th7;

then consider p being Element of T such that

A26: p in y and

A27: p is_a_convergence_point_of GG,T by A2, A23;

consider W being set such that

A28: p in W and

A29: W in F by A4, A26, TARSKI:def 4;

reconsider W = W as Subset of T by A29;

W is open by A3, A29;

then A30: W in GG by A27, A28;

A31: xF c= uparrow (fininfs xF) by WAYBEL_0:62;

x \ W in xF by A29;

then x \ W in uparrow (fininfs xF) by A31;

then ( W misses x \ W & W /\ (x \ W) in GG ) by A22, A30, Th9, XBOOLE_1:79;

then {} in GG ;

then Bottom (BoolePoset the carrier of T) in GG by YELLOW_1:18;

hence contradiction by A23, Th4; :: thesis: verum

ex p being Element of T st

( p in y & p is_a_convergence_point_of F,T ) ) holds

x << y

set B = BoolePoset the carrier of T;

let x, y be Element of (InclPoset the topology of T); :: thesis: ( x c= y & ( for F being ultra 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_convergence_point_of F,T ) ) implies x << y )

assume that

A1: x c= y and

A2: for F being ultra 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_convergence_point_of F,T ) ; :: thesis: x << y

InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;

then x in the topology of T ;

then reconsider X = x as Subset of T ;

reconsider X = X as Subset of T ;

assume not x << y ; :: thesis: contradiction

then consider F being Subset-Family of T such that

A3: F is open and

A4: y c= union F and

A5: for G being finite Subset of F holds not x c= union G by WAYBEL_3:35;

set xF = { (x \ z) where z is Subset of T : z in F } ;

set z = the Element of F;

A6: now :: thesis: not F = {}

then A8:
the Element of F in F
;assume A7:
F = {}
; :: thesis: contradiction

then y = {} by A4, ZFMISC_1:2;

then x = y by A1;

hence contradiction by A4, A5, A7; :: thesis: verum

end;then y = {} by A4, ZFMISC_1:2;

then x = y by A1;

hence contradiction by A4, A5, A7; :: thesis: verum

BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;

then A9: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def 1;

{ (x \ z) where z is Subset of T : z in F } c= the carrier of (BoolePoset the carrier of T)

proof

then reconsider xF = { (x \ z) where z is Subset of T : z in F } as Subset of (BoolePoset the carrier of T) ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (x \ z) where z is Subset of T : z in F } or a in the carrier of (BoolePoset the carrier of T) )

reconsider aa = a as set by TARSKI:1;

assume a in { (x \ z) where z is Subset of T : z in F } ; :: thesis: a in the carrier of (BoolePoset the carrier of T)

then ex z being Subset of T st

( a = x \ z & z in F ) ;

then aa c= X ;

then aa c= the carrier of T by XBOOLE_1:1;

hence a in the carrier of (BoolePoset the carrier of T) by A9; :: thesis: verum

end;reconsider aa = a as set by TARSKI:1;

assume a in { (x \ z) where z is Subset of T : z in F } ; :: thesis: a in the carrier of (BoolePoset the carrier of T)

then ex z being Subset of T st

( a = x \ z & z in F ) ;

then aa c= X ;

then aa c= the carrier of T by XBOOLE_1:1;

hence a in the carrier of (BoolePoset the carrier of T) by A9; :: thesis: verum

set FF = uparrow (fininfs xF);

now :: thesis: not Bottom (BoolePoset the carrier of T) in uparrow (fininfs xF)

then
uparrow (fininfs xF) is proper
;defpred S_{1}[ object , object ] means ex A being set st

( A = $2 & $1 = x \ A );

assume Bottom (BoolePoset the carrier of T) in uparrow (fininfs xF) ; :: thesis: contradiction

then consider a being Element of (BoolePoset the carrier of T) such that

A10: a <= Bottom (BoolePoset the carrier of T) and

A11: a in fininfs xF by WAYBEL_0:def 16;

consider s being finite Subset of xF such that

A12: a = "/\" (s,(BoolePoset the carrier of T)) and

ex_inf_of s, BoolePoset the carrier of T by A11;

reconsider t = s as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;

A14: ( dom f = s & rng f c= F & ( for v being object st v in s holds

S_{1}[v,f . v] ) )
from FUNCT_1:sch 6(A13);

reconsider G = rng f as finite Subset of F by A14, FINSET_1:8;

Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;

then A15: a c= {} by A10, YELLOW_1:2;

x c= union G

end;( A = $2 & $1 = x \ A );

assume Bottom (BoolePoset the carrier of T) in uparrow (fininfs xF) ; :: thesis: contradiction

then consider a being Element of (BoolePoset the carrier of T) such that

A10: a <= Bottom (BoolePoset the carrier of T) and

A11: a in fininfs xF by WAYBEL_0:def 16;

consider s being finite Subset of xF such that

A12: a = "/\" (s,(BoolePoset the carrier of T)) and

ex_inf_of s, BoolePoset the carrier of T by A11;

reconsider t = s as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;

A13: now :: thesis: for v being object st v in s holds

ex z being object st

( z in F & S_{1}[v,z] )

consider f being Function such that ex z being object st

( z in F & S

let v be object ; :: thesis: ( v in s implies ex z being object st

( z in F & S_{1}[v,z] ) )

assume v in s ; :: thesis: ex z being object st

( z in F & S_{1}[v,z] )

then v in xF ;

then ex z being Subset of T st

( v = x \ z & z in F ) ;

hence ex z being object st

( z in F & S_{1}[v,z] )
; :: thesis: verum

end;( z in F & S

assume v in s ; :: thesis: ex z being object st

( z in F & S

then v in xF ;

then ex z being Subset of T st

( v = x \ z & z in F ) ;

hence ex z being object st

( z in F & S

A14: ( dom f = s & rng f c= F & ( for v being object st v in s holds

S

reconsider G = rng f as finite Subset of F by A14, FINSET_1:8;

Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;

then A15: a c= {} by A10, YELLOW_1:2;

A16: now :: thesis: not s = {}

then A17:
a = meet t
by A12, YELLOW_1:20;assume
s = {}
; :: thesis: contradiction

then a = Top (BoolePoset the carrier of T) by A12;

hence contradiction by A15, YELLOW_1:19; :: thesis: verum

end;then a = Top (BoolePoset the carrier of T) by A12;

hence contradiction by A15, YELLOW_1:19; :: thesis: verum

x c= union G

proof

hence
contradiction
by A5; :: thesis: verum
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in x or c in union G )

assume that

A18: c in x and

A19: not c in union G ; :: thesis: contradiction

end;assume that

A18: c in x and

A19: not c in union G ; :: thesis: contradiction

now :: thesis: for v being set st v in s holds

c in v

hence
contradiction
by A15, A16, A17, SETFAM_1:def 1; :: thesis: verumc in v

let v be set ; :: thesis: ( v in s implies c in v )

assume A20: v in s ; :: thesis: c in v

then f . v in rng f by A14, FUNCT_1:def 3;

then A21: not c in f . v by A19, TARSKI:def 4;

S_{1}[v,f . v]
by A14, A20;

then v = x \ (f . v) ;

hence c in v by A18, A21, XBOOLE_0:def 5; :: thesis: verum

end;assume A20: v in s ; :: thesis: c in v

then f . v in rng f by A14, FUNCT_1:def 3;

then A21: not c in f . v by A19, TARSKI:def 4;

S

then v = x \ (f . v) ;

hence c in v by A18, A21, XBOOLE_0:def 5; :: thesis: verum

then consider GG being Filter of (BoolePoset the carrier of T) such that

A22: uparrow (fininfs xF) c= GG and

A23: GG is ultra by Th26;

reconsider z = the Element of F as Subset of T by A8;

A24: xF c= uparrow (fininfs xF) by WAYBEL_0:62;

x \ z in xF by A6;

then A25: x \ z in uparrow (fininfs xF) by A24;

x \ z c= X ;

then x in GG by A22, A25, Th7;

then consider p being Element of T such that

A26: p in y and

A27: p is_a_convergence_point_of GG,T by A2, A23;

consider W being set such that

A28: p in W and

A29: W in F by A4, A26, TARSKI:def 4;

reconsider W = W as Subset of T by A29;

W is open by A3, A29;

then A30: W in GG by A27, A28;

A31: xF c= uparrow (fininfs xF) by WAYBEL_0:62;

x \ W in xF by A29;

then x \ W in uparrow (fininfs xF) by A31;

then ( W misses x \ W & W /\ (x \ W) in GG ) by A22, A30, Th9, XBOOLE_1:79;

then {} in GG ;

then Bottom (BoolePoset the carrier of T) in GG by YELLOW_1:18;

hence contradiction by A23, Th4; :: thesis: verum