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 4;
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:
assume A2: x c= y ; :: thesis:
A3: B c= the topology of T by TOPS_2:64;

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 A3; :: according to PRE_TOPC:def 2 :: thesis:

end;

end;

deffunc H₁( set ) -> Element of bool x = x \ $1;
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:
defpred S₁[ object , object ] means ex A being set st
( A = $2 & $1 in A & not $2 in F );

let p be object ; :: thesis:
assume A12: 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, 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 ;
A in the topology of T by A13;
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 3;
ay c= A by A17, A19, ZFMISC_1:74;
then not ay in F by A15, Th7;
then BY is not Subset of F by A21, A22, Th11;
then consider r being object such that
A23: ( r in BY & not r in F ) by TARSKI:def 3;
reconsider A = r as set by TARSKI:1;
take r = r; :: thesis:
thus r in B by A20, A23; :: thesis:
thus S₁[p,r] :: thesis:

take A ; :: thesis:
thus ( A = r & p in A & not r in F ) by A18, A22, A23, SETFAM_1:43; :: thesis:

end;

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

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: p in y ; :: thesis:
then consider A being set such that
A27: ( A = f . p & p in A & not f . p in F ) by A25;
( f . p in FF & p in f . p ) by A24, FUNCT_1:def 3, A27, A26;
hence p in union FF by TARSKI:def 4; :: thesis:

end;

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

let a be object ; :: according to TARSKI:def 3 :: thesis:
A31: F is prime by Th22;
assume a in rng g ; :: thesis:
then consider b being object such that
A32: b in G and
A33: a = g . b by A29, FUNCT_1:def 3;
b in FF by A32;
then b in B ;
then reconsider b = b as Subset of T ;
consider p being object such that
A34: ( p in y & b = f . p ) by A24, A32, FUNCT_1:def 3;
S₁[p,f . p] by A25, A34;
then not b in F by A34;
then A35: the carrier of T \ b in F by A31, Th21;
a = x \ b by A29, A32, A33
.= X /\ (b `) by SUBSET_1:13
.= x /\ ( the carrier of T \ b) ;
hence a in F by A9, A35, Th9; :: thesis:

end;

end;

end;

end;