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 A3: x in { (S . j) where j is Element of NAT : j <= i } ; :: thesis: x in F
consider j being Element of NAT such that
A4: ( x = S . j & j <= i ) by A3;
dom S = NAT by FUNCT_2:def 1;
then x in rng S by A4, FUNCT_1:def 5;
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 } ;
A5: 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 A6: x in NAT ; :: thesis: ex y being set st
( y in bool the carrier of T & S₁[x,y] )
reconsider i = x as Element of NAT by A6;
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
A7: for x being set st x in NAT holds
S₁[x,R . x] from FUNCT_2:sch 1(A5);
A8: for i being natural number holds { (S . j) where j is Element of NAT : j <= i } is finite

proof

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 } ;
A9: i + 1 is finite ;
deffunc H₁( set ) -> set = S . $1;
A10: { H₁(j) where j is Element of NAT : j in i + 1 } is finite from FRAENKEL:sch 21(A9);
{ (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 A11: 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 }
consider j being Element of NAT such that
A12: ( x = S . j & j <= i ) by A11;
j < i + 1 by A12, NAT_1:13;
then j in i + 1 by NAT_1:45;
hence x in { H₁(j) where j is Element of NAT : j in i + 1 } by A12; :: thesis: verum

end;

hence { (S . j) where j is Element of NAT : j <= i } is finite by A10; :: thesis: verum

end;

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 } ;
A13: S . 0 in { (S . j) where j is Element of NAT : j <= i } ;
{ (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 A14: 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 }
consider j being Element of NAT such that
A15: ( x = S . j & j <= i ) by A14;
j <= i + 1 by A15, NAT_1:13;
hence x in { (S . j) where j is Element of NAT : j <= i + 1 } by A15; :: thesis: verum

end;

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 } & meet { (S . j) where j is Element of NAT : j <= i } = R . i ) by A7, A13, SETFAM_1:7;
hence R . (i + 1) c= R . i by A7; :: thesis: verum

end;

hence R is non-ascending by KURATO_2:def 5; :: 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 } ) )
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 A16: 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 A17: x in dom R ; :: thesis: not R . x is empty
reconsider i = x as Element of NAT by A17;
set SS = { (S . j) where j is Element of NAT : j <= i } ;
( { (S . j) where j is Element of NAT : j <= i } is finite & S . 0 in { (S . j) where j is Element of NAT : j <= i } & { (S . j) where j is Element of NAT : j <= i } c= F ) by A2, A8;
then meet { (S . j) where j is Element of NAT : j <= i } <> {} by A16, FINSET_1:def 3;
hence not R . x is empty by A7; :: thesis: verum

end;

hence R is non-empty by FUNCT_1:def 15; :: 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 open & SS is finite & i in NAT ) by A8, A18, A19, ORDINAL1:def 13, TOPS_2:18;
then ( meet SS is open & R . i = meet SS ) by A7, TOPS_2:27;
hence R . i is open ; :: 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 A20: 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 } ;
A21: { (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 closed & i in NAT ) by A20, A21, ORDINAL1:def 13, TOPS_2:19;
then ( meet SS is closed & meet SS = R . i ) by A7, TOPS_2:29;
hence R . i is closed ; :: 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 13;
hence R . i = meet { (S . j) where j is Element of NAT : j <= i } by A7; :: thesis: verum