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;

A6: now :: thesis: not 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 A8: the Element of F in 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)

proof

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;

then reconsider xF = { (x \ z) where z is Subset of T : z in F } as Subset of (BoolePoset the carrier of T) ;
set FF = uparrow (fininfs xF);

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

defpred S₁[ 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;

A13: now :: thesis: for v being object st v in s holds
ex z being object st
( z in F & S₁[v,z] )

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

end;

consider f being Function such that
A14: ( dom f = s & rng f c= F & ( for v being object st v in s holds
S₁[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;

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

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 A17: a = meet t by A12, YELLOW_1:20;
x c= union G

proof

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

now :: thesis: for v being set st v in s holds
c 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₁[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;

hence contradiction by A15, A16, A17, SETFAM_1:def 1; :: thesis: verum

end;

hence contradiction by A5; :: thesis: verum

end;

then uparrow (fininfs xF) is proper ;
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