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 } ;
consider z being Element of F;

A6: now

assume A7: F = {} ; :: thesis: contradiction
then A8: y = {} by A4, ZFMISC_1:2;
then x = y by A1;
hence contradiction by A1, A4, A5, A7, A8; :: thesis: verum

end;

then A9: z in F ;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then A10: 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 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 ex z being Subset of T st
( a = x \ z & z in F ) ;
then a c= X ;
then a c= the carrier of T by XBOOLE_1:1;
hence a in the carrier of (BoolePoset the carrier of T) by A10; :: 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

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

A14: 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
A15: ( dom f = s & rng f c= F & ( for v being set st v in s holds
S₁[v,f . v] ) ) from WELLORD2:sch 1(A14);
reconsider G = rng f as finite Subset of F by A15, FINSET_1:26;
Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;
then A16: a c= {} by A11, YELLOW_1:2;

A17: now

assume s = {} ; :: thesis: contradiction
then a = Top (BoolePoset the carrier of T) by A13;
hence contradiction by A16, YELLOW_1:19; :: thesis: verum

end;

then A18: a = meet t by A13, 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 that
A19: c in x and
A20: not c in union G ; :: thesis: contradiction

now

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

end;

hence contradiction by A16, A17, A18, 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
A23: uparrow (fininfs xF) c= GG and
A24: GG is ultra by Th30;
reconsider z = z as Subset of T by A9;
A25: xF c= uparrow (fininfs xF) by WAYBEL_0:62;
x \ z in xF by A6;
then A26: x \ z in uparrow (fininfs xF) by A25;
x \ z c= X ;
then x in GG by A23, A26, Th11;
then consider p being Element of T such that
A27: p in y and
A28: p is_a_convergence_point_of GG,T by A2, A24;
consider W being set such that
A29: p in W and
A30: W in F by A4, A27, TARSKI:def 4;
reconsider W = W as Subset of T by A30;
W is open by A3, A30, TOPS_2:def 1;
then A31: W in GG by A28, A29, Def5;
A32: xF c= uparrow (fininfs xF) by WAYBEL_0:62;
x \ W in xF by A30;
then x \ W in uparrow (fininfs xF) by A32;
then ( W misses x \ W & W /\ (x \ W) in GG ) by A23, A31, Th13, XBOOLE_1:79;
then {} in GG by XBOOLE_0:def 7;
then Bottom (BoolePoset the carrier of T) in GG by YELLOW_1:18;
hence contradiction by A24, Th8; :: thesis: verum