defpred S₁[ Nat] means for T being TopSpace
for A being finite Subset of T st card A <= $1 holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) );
let T be TopSpace; :: thesis: for A being finite Subset of T holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )
let A be finite Subset of T; :: thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
let T be TopSpace; :: thesis: for A being finite Subset of T st card A <= n + 1 holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )
let A be finite Subset of T; :: thesis: ( card A <= n + 1 implies ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) )
assume A3: card A <= n + 1 ; :: thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )

per cases ( card A <= n or card A = n + 1 ) by A3, NAT_1:8;

suppose card A <= n ; :: thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )

hence ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) by A2; :: thesis: verum

end;

suppose A4: card A = n + 1 ; :: thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )

for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )

proof

let p be Point of (T | A); :: thesis: for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
let U be open Subset of (T | A); :: thesis: ( p in U implies ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) )
assume A5: p in U ; :: thesis: ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
take W = U; :: thesis: ( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
{p} c= W by A5, ZFMISC_1:31;
then A6: ( Fr W = (Cl W) \ W & A \ W c= A \ {p} ) by TOPS_1:42, XBOOLE_1:34;
thus ( p in W & W c= U ) by A5; :: thesis: Fr W in (Seq_of_ind T) . n
[#] (T | A) c= [#] T by PRE_TOPC:def 4;
then reconsider FrW = Fr W as Subset of T by XBOOLE_1:1;
A7: ( A \ {p} c= A & not p in A \ {p} ) by ZFMISC_1:56;
A8: [#] (T | A) = A by PRE_TOPC:def 5;
then p in A by A5;
then A9: A \ {p} c< A by A7;
(Cl W) \ W c= A \ W by A8, XBOOLE_1:33;
then card (Fr W) <= card (A \ {p}) by A6, NAT_1:43, XBOOLE_1:1;
then card (Fr W) < n + 1 by A4, A9, CARD_2:48, XXREAL_0:2;
then A10: card (Fr W) <= n by NAT_1:13;
then A11: Fr W in (Seq_of_ind (T | A)) . (card (Fr W)) by A2;
(Seq_of_ind (T | A)) . (card (Fr W)) c= (Seq_of_ind (T | A)) . n by A10, PROB_1:def 5;
then FrW in (Seq_of_ind T) . n by A11, Th3;
hence Fr W in (Seq_of_ind T) . n ; :: thesis: verum

end;

then A in (Seq_of_ind T) . (card A) by A4, Def1;
hence ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) ; :: thesis: verum

end;

end;

end;

A12: S₁[ 0 ]

proof

let T be TopSpace; :: thesis: for A being finite Subset of T st card A <= 0 holds
( A is finite-ind & A in (Seq_of_ind T) . (card A) )
let A be finite Subset of T; :: thesis: ( card A <= 0 implies ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) )
A13: (Seq_of_ind T) . 0 = {({} T)} by Def1;
assume A14: card A <= 0 ; :: thesis: ( A is finite-ind & A in (Seq_of_ind T) . (card A) )
then A = {} ;
then A in {({} T)} by TARSKI:def 1;
hence ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) by A13, A14; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A1);
then S₁[ card A] ;
hence ( A is finite-ind & A in (Seq_of_ind T) . (card A) ) ; :: thesis: verum