let T be non empty TopSpace; :: thesis:
let B be prebasis of T; :: thesis:
consider BB being Basis of T such that
A1: BB c= FinMeetCl B by CANTOR_1:def 5;
A2: the topology of T c= UniCl BB by CANTOR_1:def 2;
set L = InclPoset the topology of T;
set BT = BoolePoset the carrier of T;
BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then A3: ( 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:
assume A4: x c= y ; :: thesis:
( x in the topology of T & y in the topology of T ) by A3;
then reconsider X = x, Y = y as Subset of T ;
A5: B c= the topology of T by CANTOR_1:def 5;

hereby :: thesis:

assume A6: x << y ; :: thesis:
let F be Subset of B; :: thesis:
assume A7: y c= union F ; :: thesis:
reconsider FF = F as Subset-Family of T by XBOOLE_1:1;
FF is open

proof

let a be Subset of T; :: according to TOPS_2:def 1 :: thesis:
assume a in FF ; :: thesis:
then a in B ;
hence a in the topology of T by A5; :: according to PRE_TOPC:def 5 :: thesis:

end;

hence ex G being finite Subset of F st x c= union G by A6, A7, WAYBEL_3:34; :: thesis:

end;

assume A8: for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ; :: thesis:

now

let F be ultra Filter of (BoolePoset the carrier of T); :: thesis:
assume that
A9: x in F and
A10: for p being Element of T holds
( not p in y or not p is_a_convergence_point_of F,T ) ; :: thesis:
x <> Bottom (BoolePoset the carrier of T) by A9, Th8;
then A11: x <> {} by YELLOW_1:18;
defpred S₁[ set , set ] means ( $1 in $2 & not $2 in F );

A12: now

let p be set ; :: thesis:
assume A13: p in y ; :: thesis:
then p in Y ;
then reconsider q = p as Element of T ;
not q is_a_convergence_point_of F,T by A10, A13;
then consider A being Subset of T such that
A14: ( A is open & q in A & not A in F ) by Def5;
A in the topology of T by A14, PRE_TOPC:def 5;
then consider AY being Subset-Family of T such that
A15: ( AY c= BB & A = union AY ) by A2, CANTOR_1:def 1;
consider ay being set such that
A16: ( q in ay & ay in AY ) by A14, A15, TARSKI:def 4;
reconsider ay = ay as Subset of T by A16;
ay in BB by A15, A16;
then consider BY being Subset-Family of T such that
A17: ( BY c= B & BY is finite & ay = Intersect BY ) by A1, CANTOR_1:def 4;
ay c= A by A15, A16, ZFMISC_1:92;
then not ay in F by A14, Th11;
then BY is not Subset of F by A17, Th15;
then consider r being set such that
A18: ( r in BY & not r in F ) by TARSKI:def 3;
take r = r; :: thesis:
thus ( r in B & S₁[p,r] ) by A16, A17, A18, SETFAM_1:58; :: thesis:

end;

consider f being Function such that
A19: ( dom f = y & rng f c= B ) and
A20: for p being set st p in y holds
S₁[p,f . p] from WELLORD2:sch 1(A12);
reconsider FF = rng f as Subset of B by A19;
y c= union FF

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume p in y ; :: thesis:
then ( f . p in FF & p in f . p ) by A19, A20, FUNCT_1:def 5;
hence p in union FF by TARSKI:def 4; :: thesis:

end;

then consider G being finite Subset of FF such that
A21: x c= union G by A8;
A22: G <> {} by A11, A21, ZFMISC_1:2;
consider gg being Element of G;
deffunc H₁( set ) -> Element of bool x = x \ $1;
consider g being Function such that
A23: ( dom g = G & ( for z being set st z in G holds
g . z = H₁(z) ) ) from FUNCT_1:sch 3();
A24: rng g c= F

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng g ; :: thesis:
then consider b being set such that
A25: ( b in G & a = g . b ) by A23, FUNCT_1:def 5;
b in FF by A25;
then b in B ;
then reconsider b = b as Subset of T ;
A26: a = x \ b by A23, A25
.= X /\ (b ` ) by SUBSET_1:32
.= x /\ (the carrier of T \ b) ;
consider p being set such that
A27: ( p in y & b = f . p ) by A19, A25, FUNCT_1:def 5;
( not b in F & F is prime ) by A20, A27, Th26;
then the carrier of T \ b in F by Th25;
hence a in F by A9, A26, Th13; :: thesis:

end;

then reconsider GG = rng g as finite Subset-Family of T by A3, A23, FINSET_1:26, XBOOLE_1:1;
A28: Intersect GG in F by A24, Th15;

now

let a be set ; :: thesis:
assume A29: a in Intersect GG ; :: thesis:

now

let z be set ; :: thesis:
assume z in G ; :: thesis:
then ( g . z in GG & g . z = x \ z ) by A23, FUNCT_1:def 5;
then a in x \ z by A29, SETFAM_1:58;
hence not a in z by XBOOLE_0:def 5; :: thesis:

end;

then for z being set holds
( not a in z or not z in G ) ;
then ( not a in union G & g . gg in GG & g . gg = x \ gg ) by A22, A23, FUNCT_1:def 5, TARSKI:def 4;
then ( not a in x & a in x \ gg ) by A21, A29, SETFAM_1:58;
hence contradiction ; :: thesis:

end;

then Intersect GG = {} by XBOOLE_0:def 1;
then Bottom (BoolePoset the carrier of T) in F by A28, YELLOW_1:18;
hence contradiction by Th8; :: thesis:

end;

hence x << y by A4, Th34; :: thesis: