consider K being prebasis of F1() such that
A5:
for A being Subset of F1() st A in K holds
P1[A]
by A1;
let A be Subset of F1(); ( A is open implies P1[A] )
assume A6:
A in the topology of F1()
; PRE_TOPC:def 2 P1[A]
FinMeetCl K is Basis of F1()
by YELLOW_9:23;
then
UniCl (FinMeetCl K) = the topology of F1()
by YELLOW_9:22;
then consider X being Subset-Family of F1() 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 F1() ;
now for A being Subset of F1() st A in X holds
P1[A]defpred S1[
set ]
means for
a being
Subset-Family of
F1() st
a = $1 holds
P1[
Intersect a];
let A be
Subset of
F1();
( A in X implies P1[A] )assume
A in X
;
P1[A]then consider Y being
Subset-Family of
F1()
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 &
S1[
Z] holds
S1[
Z \/ {x}]
proof
let x,
Z be
set ;
( x in Y & Z c= Y & S1[Z] implies S1[Z \/ {x}] )
assume that A13:
x in Y
and A14:
Z c= Y
and A15:
S1[
Z]
;
S1[Z \/ {x}]
reconsider xx =
{x},
Z9 =
Z as
Subset-Family of
F1()
by A13, A14, XBOOLE_1:1, ZFMISC_1:31;
reconsider xx =
xx,
Z9 =
Z9 as
Subset-Family of
F1() ;
reconsider xx =
xx,
Z9 =
Z9 as
Subset-Family of
F1() ;
reconsider Ax =
x,
Ay =
Intersect Z9 as
Subset of
F1()
by A13;
A16:
P1[
Ay]
by A15;
let a be
Subset-Family of
F1();
( a = Z \/ {x} implies P1[ Intersect a] )
assume A17:
a = Z \/ {x}
;
P1[ Intersect a]
Intersect xx = Ax
by MSSUBFAM:9;
then A18:
Intersect a = Ax /\ Ay
by A17, MSSUBFAM:8;
P1[
Ax]
by A5, A9, A13;
hence
P1[
Intersect a]
by A18, A3, A16;
verum
end; A19:
S1[
{} ]
by A4, SETFAM_1:def 9;
S1[
Y]
from FINSET_1:sch 2(A10, A19, A12);
hence
P1[
A]
by A11;
verum end;
hence
P1[A]
by A2, A8; verum