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 Nat 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 Nat 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 Nat 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 Nat holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )
A2: for i being Nat holds { (S . j) where j is Element of NAT : j <= i } c= F

proof

let i be Nat; :: thesis: { (S . j) where j is Element of NAT : j <= i } c= F
let x be object ; :: 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 consider j being Element of NAT such that
A3: ( 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₁[ object , object ] means for i being Nat st i = $1 holds
$2 = meet { (S . j) where j is Element of NAT : j <= i } ;
A4: for x being object st x in NAT holds
ex y being object st
( y in bool the carrier of T & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in bool the carrier of T & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object 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 object 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 Nat holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )

now :: thesis: for i being Nat holds R . (i + 1) c= R . i

let i be Nat; :: thesis: R . (i + 1) c= R . i
A6: i in NAT by ORDINAL1:def 12;
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 } ;
A7: { (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 object ; :: 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
A8: x = S . j and
A9: j <= i ;
j <= i + 1 by A9, NAT_1:13;
hence x in { (S . j) where j is Element of NAT : j <= i + 1 } by A8; :: thesis: verum

end;

A10: meet { (S . j) where j is Element of NAT : j <= i } = R . i by A5, A6;
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 A7, SETFAM_1:6;
hence R . (i + 1) c= R . i by A5, A10; :: 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 Nat holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )
A11: for i being Nat holds { (S . j) where j is Element of NAT : j <= i } is finite

proof

deffunc H₁( set ) -> set = S . $1;
let i be Nat; :: 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 } ;
A12: { (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 object ; :: 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
A13: x = S . j and
A14: j <= i ;
j < i + 1 by A14, NAT_1:13;
then j in Segm (i + 1) by NAT_1:44;
hence x in { H₁(j) where j is Element of NAT : j in i + 1 } by A13; :: thesis: verum

end;

A15: i + 1 is finite ;
{ H₁(j) where j is Element of NAT : j in i + 1 } is finite from FRAENKEL:sch 21(A15);
hence { (S . j) where j is Element of NAT : j <= i } is finite by A12; :: 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 Nat holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )

proof

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

now :: thesis: for x being object st x in dom R holds
not R . x is empty

let x be object ; :: 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 } ;
A17: S . 0 in { (S . j) where j is Element of NAT : j <= i } ;
A18: { (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 A11;
then meet { (S . j) where j is Element of NAT : j <= i } <> {} by A16, A17, A18, 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 Nat holds R . i = meet { (S . j) where j is Element of NAT : j <= i } ) )

proof

assume A19: F is open ; :: thesis: R is open
let i be Nat; :: according to COMPL_SP:def 5 :: thesis: R . i is open
set SS = { (S . j) where j is Element of NAT : j <= i } ;
A20: { (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 A11;
then A21: meet SS is open by A19, A20, TOPS_2:11, TOPS_2:20;
i in NAT by ORDINAL1:def 12;
hence R . i is open by A5, A21; :: thesis: verum

end;

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

proof

assume A22: F is closed ; :: thesis: R is closed
let i be Nat; :: according to COMPL_SP:def 6 :: thesis: R . i is closed
set SS = { (S . j) where j is Element of NAT : j <= i } ;
A23: i in NAT by ORDINAL1:def 12;
A24: { (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 A22, A24, TOPS_2:12, TOPS_2:22;
hence R . i is closed by A5, A23; :: thesis: verum

end;

let i be Nat; :: 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