let T be non empty TopSpace; :: thesis: for B being prebasis of T
for x, y being Element of (InclPoset the topology of T) st x c= y holds
( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
let B be prebasis of T; :: thesis: for x, y being Element of (InclPoset the topology of T) st x c= y holds
( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
consider BB being Basis of T such that
A1: BB c= FinMeetCl B by CANTOR_1:def 5;
set BT = BoolePoset the carrier of T;
set L = InclPoset the topology of T;
let x, y be Element of (InclPoset the topology of T); :: thesis: ( x c= y implies ( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ) )
assume A2: x c= y ; :: thesis: ( x << y iff for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G )
A3: B c= the topology of T by TOPS_2:78;

hereby :: thesis: ( ( for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G ) implies x << y )

assume A4: x << y ; :: thesis: for F being Subset of B st y c= union F holds
ex G being finite Subset of F st x c= union G
let F be Subset of B; :: thesis: ( y c= union F implies ex G being finite Subset of F st x c= union G )
assume A5: y c= union F ; :: thesis: ex G being finite Subset of F st x c= union G
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: ( not a in FF or a is open )
assume a in FF ; :: thesis: a is open
then a in B ;
hence a in the topology of T by A3; :: according to PRE_TOPC:def 5 :: thesis: verum

end;

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

end;

BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4;
then A6: BoolePoset the carrier of T = RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def 1;
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 & y in the topology of T ) ;
then reconsider X = x, Y = y as Subset of T ;
assume A7: 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: x << y
A8: the topology of T c= UniCl BB by CANTOR_1:def 2;

now

deffunc H₁( set ) -> Element of bool x = x \ $1;
let F be ultra Filter of (BoolePoset the carrier of T); :: thesis: ( x in F implies ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) )
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: contradiction
defpred S₁[ set , set ] means ( $1 in $2 & not $2 in F );

A11: now

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

end;

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

proof

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

end;

then consider G being finite Subset of FF such that
A26: x c= union G by A7;
consider gg being Element of G;
consider g being Function such that
A27: ( dom g = G & ( for z being set st z in G holds
g . z = H₁(z) ) ) from FUNCT_1:sch 3();
A28: rng g c= F

proof

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

end;

then reconsider GG = rng g as finite Subset-Family of T by A6, A27, FINSET_1:26, XBOOLE_1:1;
x <> Bottom (BoolePoset the carrier of T) by A9, Th8;
then x <> {} by YELLOW_1:18;
then A33: G <> {} by A26, ZFMISC_1:2;

now

let a be set ; :: thesis: not a in Intersect GG
assume A34: a in Intersect GG ; :: thesis: contradiction

now

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

end;

then for z being set holds
( not a in z or not z in G ) ;
then A35: not a in x by A26, TARSKI:def 4;
( g . gg in GG & g . gg = x \ gg ) by A33, A27, FUNCT_1:def 5;
then a in x \ gg by A34, SETFAM_1:58;
hence contradiction by A35; :: thesis: verum

end;

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

end;

hence x << y by A2, Th34; :: thesis: verum