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;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then A1: ( InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) & BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) ) by YELLOW_1:def 1;
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
A2: x c= y and
A3: 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
x in the topology of T by A1;
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
A4: ( F is open & 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 } ;
{ (x \ z) where z is Subset of T : z in F } c= the carrier of (BoolePoset the carrier of T)

proof

let a be set ; :: 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) )
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 consider z being Subset of T such that
A6: ( a = x \ z & z in F ) ;
a c= X by A6;
then a c= the carrier of T by XBOOLE_1:1;
hence a in the carrier of (BoolePoset the carrier of T) by A1; :: 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

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
A7: ( a <= Bottom (BoolePoset the carrier of T) & a in fininfs xF ) by WAYBEL_0:def 16;
consider s being finite Subset of xF such that
A8: ( a = "/\" s,(BoolePoset the carrier of T) & ex_inf_of s, BoolePoset the carrier of T ) by A7;
reconsider t = s as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1;
defpred S₁[ set , set ] means $1 = x \ $2;

A9: now

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

end;

consider f being Function such that
A10: ( dom f = s & rng f c= F & ( for v being set st v in s holds
S₁[v,f . v] ) ) from WELLORD2:sch 1(A9);
reconsider G = rng f as finite Subset of F by A10, FINSET_1:26;
Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;
then a c= {} by A7, YELLOW_1:2;
then A11: a = {} ;

A12: now

assume s = {} ; :: thesis: contradiction
then ( a = Top (BoolePoset the carrier of T) & the carrier of T <> {} ) by A8;
hence contradiction by A11, YELLOW_1:19; :: thesis: verum

end;

then A13: a = meet t by A8, YELLOW_1:20;
x c= union G

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in x or c in union G )
assume A14: ( c in x & not c in union G ) ; :: thesis: contradiction

now

let v be set ; :: thesis: ( v in s implies c in v )
assume A15: v in s ; :: thesis: c in v
then f . v in rng f by A10, FUNCT_1:def 5;
then ( v = x \ (f . v) & not c in f . v ) by A10, A14, A15, TARSKI:def 4;
hence c in v by A14, XBOOLE_0:def 5; :: thesis: verum

end;

hence contradiction by A11, A12, A13, SETFAM_1:def 1; :: thesis: verum

end;

hence contradiction by A5; :: thesis: verum

end;

then uparrow (fininfs xF) is proper by Th8;
then consider GG being Filter of (BoolePoset the carrier of T) such that
A16: ( uparrow (fininfs xF) c= GG & GG is ultra ) by Th30;
consider z being Element of F;

A17: now

assume A18: F = {} ; :: thesis: contradiction
then y = {} by A4, ZFMISC_1:2;
then ( x = y & F is finite Subset of F ) by A2, A18;
hence contradiction by A4, A5; :: thesis: verum

end;

then z in F ;
then reconsider z = z as Subset of T ;
( x \ z in xF & xF c= uparrow (fininfs xF) ) by A17, WAYBEL_0:62;
then ( x \ z in uparrow (fininfs xF) & x \ z c= X ) ;
then x in GG by A16, Th11;
then consider p being Element of T such that
A19: ( p in y & p is_a_convergence_point_of GG,T ) by A3, A16;
consider W being set such that
A20: ( p in W & W in F ) by A4, A19, TARSKI:def 4;
reconsider W = W as Subset of T by A20;
W is open by A4, A20, TOPS_2:def 1;
then A21: W in GG by A19, A20, Def5;
A22: W misses x \ W by XBOOLE_1:79;
( x \ W in xF & xF c= uparrow (fininfs xF) ) by A20, WAYBEL_0:62;
then x \ W in uparrow (fininfs xF) ;
then W /\ (x \ W) in GG by A16, A21, Th13;
then {} in GG by A22, XBOOLE_0:def 7;
then ( Bottom (BoolePoset the carrier of T) in GG & GG is ultra Filter of (BoolePoset the carrier of T) ) by A16, YELLOW_1:18;
hence contradiction by Th8; :: thesis: verum