consider K being prebasis of F₁() such that
A5: for A being Subset of F₁() st A in K holds
P₁[A] by A1;
let A be Subset of F₁(); :: thesis: ( A is open implies P₁[A] )
assume A6: A in the topology of F₁() ; :: according to PRE_TOPC:def 2 :: thesis: P₁[A]
FinMeetCl K is Basis of F₁() by YELLOW_9:23;
then UniCl (FinMeetCl K) = the topology of F₁() by YELLOW_9:22;
then consider X being Subset-Family of F₁() such that
A7: X c= FinMeetCl K and
A8: A = union X by A6, CANTOR_1:def 1;
reconsider X = X as Subset-Family of F₁() ;

now :: thesis: for A being Subset of F₁() st A in X holds
P₁[A]

defpred S₁[ set ] means for a being Subset-Family of F₁() st a = $1 holds
P₁[ Intersect a];
let A be Subset of F₁(); :: thesis: ( A in X implies P₁[A] )
assume A in X ; :: thesis: P₁[A]
then consider Y being Subset-Family of F₁() such that
A9: Y c= K and
A10: Y is finite and
A11: A = Intersect Y by A7, CANTOR_1:def 3;
A12: for x, Z being set st x in Y & Z c= Y & S₁[Z] holds
S₁[Z \/ {x}]

proof

let x, Z be set ; :: thesis: ( x in Y & Z c= Y & S₁[Z] implies S₁[Z \/ {x}] )
assume that
A13: x in Y and
A14: Z c= Y and
A15: S₁[Z] ; :: thesis: S₁[Z \/ {x}]
reconsider xx = {x}, Z9 = Z as Subset-Family of F₁() by A13, A14, XBOOLE_1:1, ZFMISC_1:31;
reconsider xx = xx, Z9 = Z9 as Subset-Family of F₁() ;
reconsider xx = xx, Z9 = Z9 as Subset-Family of F₁() ;
reconsider Ax = x, Ay = Intersect Z9 as Subset of F₁() by A13;
A16: P₁[Ay] by A15;
let a be Subset-Family of F₁(); :: thesis: ( a = Z \/ {x} implies P₁[ Intersect a] )
assume A17: a = Z \/ {x} ; :: thesis: P₁[ Intersect a]
Intersect xx = Ax by MSSUBFAM:9;
then A18: Intersect a = Ax /\ Ay by A17, MSSUBFAM:8;
P₁[Ax] by A5, A9, A13;
hence P₁[ Intersect a] by A18, A3, A16; :: thesis: verum

end;

A19: S₁[ {} ] by A4, SETFAM_1:def 9;
S₁[Y] from FINSET_1:sch 2(A10, A19, A12);
hence P₁[A] by A11; :: thesis: verum

end;

hence P₁[A] by A2, A8; :: thesis: verum