let T be non empty TopSpace; :: thesis: for F being Subset-Family of T
for S being SetSequence of T st rng S c= F holds
ex R being SetSequence of T st
( R is non-ascending & ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )
let F be Subset-Family of T; :: thesis: for S being SetSequence of T st rng S c= F holds
ex R being SetSequence of T st
( R is non-ascending & ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )
let S be SetSequence of T; :: thesis: ( rng S c= F implies ex R being SetSequence of T st
( R is non-ascending & ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) ) )
assume A1: rng S c= F ; :: thesis: ex R being SetSequence of T st
( R is non-ascending & ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )
A2: for i being natural number holds { (S . j) where j is Element of NAT : j <= i } c= F

proof

let i be natural number ; :: thesis: { (S . j) where j is Element of NAT : j <= i } c= F
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (S . j) where j is Element of NAT : j <= i } or x in F )
assume x in { (S . j) where j is Element of NAT : j <= i } ; :: thesis: x in F
then A3: ex j being Element of NAT st
( x = S . j & j <= i ) ;
dom S = NAT by FUNCT_2:def 1;
then x in rng S by A3, FUNCT_1:def 3;
hence x in F by A1; :: thesis: verum

end;

defpred S₁[ set , set ] means for i being natural number st i = $1 holds
$2 = meet { (S . j) where j is Element of NAT : j <= i } ;
A4: for x being set st x in NAT holds
ex y being set st
( y in bool the carrier of T & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in bool the carrier of T & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in bool the carrier of T & S₁[x,y] )
then reconsider i = x as Element of NAT ;
set SS = { (S . j) where j is Element of NAT : j <= i } ;
{ (S . j) where j is Element of NAT : j <= i } c= F by A2;
then reconsider SS = { (S . j) where j is Element of NAT : j <= i } as Subset-Family of T by XBOOLE_1:1;
take meet SS ; :: thesis: ( meet SS in bool the carrier of T & S₁[x, meet SS] )
thus ( meet SS in bool the carrier of T & S₁[x, meet SS] ) ; :: thesis: verum

end;

consider R being SetSequence of T such that
A5: for x being set st x in NAT holds
S₁[x,R . x] from FUNCT_2:sch 1(A4);
take R ; :: thesis: ( R is non-ascending & ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )

now

let i be Element of NAT ; :: thesis: R . (i + 1) c= R . i
set SS = { (S . j) where j is Element of NAT : j <= i } ;
set S1 = { (S . j) where j is Element of NAT : j <= i + 1 } ;
A6: { (S . j) where j is Element of NAT : j <= i } c= { (S . j) where j is Element of NAT : j <= i + 1 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (S . j) where j is Element of NAT : j <= i } or x in { (S . j) where j is Element of NAT : j <= i + 1 } )
assume x in { (S . j) where j is Element of NAT : j <= i } ; :: thesis: x in { (S . j) where j is Element of NAT : j <= i + 1 }
then consider j being Element of NAT such that
A7: x = S . j and
A8: j <= i ;
j <= i + 1 by A8, NAT_1:13;
hence x in { (S . j) where j is Element of NAT : j <= i + 1 } by A7; :: thesis: verum

end;

A9: meet { (S . j) where j is Element of NAT : j <= i } = R . i by A5;
S . 0 in { (S . j) where j is Element of NAT : j <= i } ;
then meet { (S . j) where j is Element of NAT : j <= i + 1 } c= meet { (S . j) where j is Element of NAT : j <= i } by A6, SETFAM_1:6;
hence R . (i + 1) c= R . i by A5, A9; :: thesis: verum

end;

hence R is non-ascending by KURATO_0:def 3; :: thesis: ( ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )
A10: for i being natural number holds { (S . j) where j is Element of NAT : j <= i } is finite

proof

deffunc H₁( set ) -> set = S . $1;
let i be natural number ; :: thesis: { (S . j) where j is Element of NAT : j <= i } is finite
set SS = { (S . j) where j is Element of NAT : j <= i } ;
A11: { (S . j) where j is Element of NAT : j <= i } c= { H₁(j) where j is Element of NAT : j in i + 1 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (S . j) where j is Element of NAT : j <= i } or x in { H₁(j) where j is Element of NAT : j in i + 1 } )
assume x in { (S . j) where j is Element of NAT : j <= i } ; :: thesis: x in { H₁(j) where j is Element of NAT : j in i + 1 }
then consider j being Element of NAT such that
A12: x = S . j and
A13: j <= i ;
j < i + 1 by A13, NAT_1:13;
then j in i + 1 by NAT_1:44;
hence x in { H₁(j) where j is Element of NAT : j in i + 1 } by A12; :: thesis: verum

end;

A14: i + 1 is finite ;
{ H₁(j) where j is Element of NAT : j in i + 1 } is finite from FRAENKEL:sch 21(A14);
hence { (S . j) where j is Element of NAT : j <= i } is finite by A11; :: thesis: verum

end;

thus ( F is centered implies R is non-empty ) :: thesis: ( ( F is open implies R is open ) & ( F is closed implies R is closed ) & ( for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )

proof

assume A15: F is centered ; :: thesis: R is non-empty

now

let x be set ; :: thesis: ( x in dom R implies not R . x is empty )
assume x in dom R ; :: thesis: not R . x is empty
then reconsider i = x as Element of NAT ;
set SS = { (S . j) where j is Element of NAT : j <= i } ;
A16: S . 0 in { (S . j) where j is Element of NAT : j <= i } ;
A17: { (S . j) where j is Element of NAT : j <= i } c= F by A2;
{ (S . j) where j is Element of NAT : j <= i } is finite by A10;
then meet { (S . j) where j is Element of NAT : j <= i } <> {} by A15, A16, A17, FINSET_1:def 3;
hence not R . x is empty by A5; :: thesis: verum

end;

hence R is non-empty by FUNCT_1:def 9; :: thesis: verum

end;

thus ( F is open implies R is open ) :: thesis: ( ( F is closed implies R is closed ) & ( for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )

proof

assume A18: F is open ; :: thesis: R is open
let i be natural number ; :: according to COMPL_SP:def 5 :: thesis: R . i is open
set SS = { (S . j) where j is Element of NAT : j <= i } ;
A19: { (S . j) where j is Element of NAT : j <= i } c= F by A2;
then reconsider SS = { (S . j) where j is Element of NAT : j <= i } as Subset-Family of T by XBOOLE_1:1;
SS is finite by A10;
then A20: meet SS is open by A18, A19, TOPS_2:11, TOPS_2:20;
i in NAT by ORDINAL1:def 12;
hence R . i is open by A5, A20; :: thesis: verum

end;

thus ( F is closed implies R is closed ) :: thesis: for i being natural number holds R . i = meet { (S . j) where j is Element of NAT : j <= i }

proof

assume A21: F is closed ; :: thesis: R is closed
let i be natural number ; :: according to COMPL_SP:def 6 :: thesis: R . i is closed
set SS = { (S . j) where j is Element of NAT : j <= i } ;
A22: i in NAT by ORDINAL1:def 12;
A23: { (S . j) where j is Element of NAT : j <= i } c= F by A2;
then reconsider SS = { (S . j) where j is Element of NAT : j <= i } as Subset-Family of T by XBOOLE_1:1;
meet SS is closed by A21, A23, TOPS_2:12, TOPS_2:22;
hence R . i is closed by A5, A22; :: thesis: verum

end;

let i be natural number ; :: thesis: R . i = meet { (S . j) where j is Element of NAT : j <= i }
i in NAT by ORDINAL1:def 12;
hence R . i = meet { (S . j) where j is Element of NAT : j <= i } by A5; :: thesis: verum