let T be TopSpace; :: thesis: for A, B being Subset of T
for n being Nat
for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )
let A, B be Subset of T; :: thesis: for n being Nat
for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )
let n be Nat; :: thesis: for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n )
defpred S₁[ Nat] means for F being Subset of (T | A)
for B being Subset of T st F = B holds
( F in (Seq_of_ind (T | A)) . $1 iff B in (Seq_of_ind T) . $1 );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

set TA = T | A;
let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let F be Subset of (T | A); :: thesis: for B being Subset of T st F = B holds
( F in (Seq_of_ind (T | A)) . (n + 1) iff B in (Seq_of_ind T) . (n + 1) )
let B be Subset of T; :: thesis: ( F = B implies ( F in (Seq_of_ind (T | A)) . (n + 1) iff B in (Seq_of_ind T) . (n + 1) ) )
assume A3: F = B ; :: thesis: ( F in (Seq_of_ind (T | A)) . (n + 1) iff B in (Seq_of_ind T) . (n + 1) )
set TAF = (T | A) | F;
set TB = T | B;
A4: (T | A) | F = T | B by A3, METRIZTS:9;
A5: [#] (T | B) c= [#] T by PRE_TOPC:def 4;

hereby :: thesis: ( B in (Seq_of_ind T) . (n + 1) implies F in (Seq_of_ind (T | A)) . (n + 1) )

assume A6: F in (Seq_of_ind (T | A)) . (n + 1) ; :: thesis: B in (Seq_of_ind T) . (n + 1)

per cases ( F in (Seq_of_ind (T | A)) . n or for p being Point of ((T | A) | F)
for U being open Subset of ((T | A) | F) st p in U holds
ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n ) ) by A6, Def1;

suppose F in (Seq_of_ind (T | A)) . n ; :: thesis: B in (Seq_of_ind T) . (n + 1)

then B in (Seq_of_ind T) . n by A2, A3;
hence B in (Seq_of_ind T) . (n + 1) by Def1; :: thesis: verum

end;

suppose A7: for p being Point of ((T | A) | F)
for U being open Subset of ((T | A) | F) st p in U holds
ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n ) ; :: thesis: B in (Seq_of_ind T) . (n + 1)

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

let p be Point of (T | B); :: thesis: for U being open Subset of (T | B) st p in U holds
ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
let U be open Subset of (T | B); :: thesis: ( p in U implies ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) )
assume A8: p in U ; :: thesis: ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
reconsider U9 = U as open Subset of ((T | A) | F) by A4;
consider W9 being open Subset of ((T | A) | F) such that
A9: ( p in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind (T | A)) . n ) by A7, A8;
reconsider W = W9 as open Subset of (T | B) by A4;
take W = W; :: thesis: ( p in W & W c= U & Fr W in (Seq_of_ind T) . n )
Fr W is Subset of T by A5, XBOOLE_1:1;
hence ( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) by A2, A4, A9; :: thesis: verum

end;

hence B in (Seq_of_ind T) . (n + 1) by Def1; :: thesis: verum

end;

end;

end;

A10: [#] ((T | A) | F) c= [#] (T | A) by PRE_TOPC:def 4;
assume A11: B in (Seq_of_ind T) . (n + 1) ; :: thesis: F in (Seq_of_ind (T | A)) . (n + 1)

per cases ( B in (Seq_of_ind T) . n or for p being Point of (T | B)
for U being open Subset of (T | B) st p in U holds
ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) ) by A11, Def1;

suppose B in (Seq_of_ind T) . n ; :: thesis: F in (Seq_of_ind (T | A)) . (n + 1)

then F in (Seq_of_ind (T | A)) . n by A2, A3;
hence F in (Seq_of_ind (T | A)) . (n + 1) by Def1; :: thesis: verum

end;

suppose A12: for p being Point of (T | B)
for U being open Subset of (T | B) st p in U holds
ex W being open Subset of (T | B) st
( p in W & W c= U & Fr W in (Seq_of_ind T) . n ) ; :: thesis: F in (Seq_of_ind (T | A)) . (n + 1)

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

let p be Point of ((T | A) | F); :: thesis: for U being open Subset of ((T | A) | F) st p in U holds
ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n )
let U be open Subset of ((T | A) | F); :: thesis: ( p in U implies ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n ) )
assume A13: p in U ; :: thesis: ex W being open Subset of ((T | A) | F) st
( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n )
reconsider U9 = U as open Subset of (T | B) by A4;
consider W9 being open Subset of (T | B) such that
A14: ( p in W9 & W9 c= U9 & Fr W9 in (Seq_of_ind T) . n ) by A12, A13;
reconsider W = W9 as open Subset of ((T | A) | F) by A4;
take W = W; :: thesis: ( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n )
Fr W is Subset of (T | A) by A10, XBOOLE_1:1;
hence ( p in W & W c= U & Fr W in (Seq_of_ind (T | A)) . n ) by A2, A4, A14; :: thesis: verum

end;

hence F in (Seq_of_ind (T | A)) . (n + 1) by Def1; :: thesis: verum

end;

end;

end;

A15: S₁[ 0 ]

proof

A16: (Seq_of_ind (T | A)) . 0 = {({} (T | A))} by Def1
.= {({} T)}
.= (Seq_of_ind T) . 0 by Def1 ;
let F be Subset of (T | A); :: thesis: for B being Subset of T st F = B holds
( F in (Seq_of_ind (T | A)) . 0 iff B in (Seq_of_ind T) . 0 )
let B be Subset of T; :: thesis: ( F = B implies ( F in (Seq_of_ind (T | A)) . 0 iff B in (Seq_of_ind T) . 0 ) )
assume F = B ; :: thesis: ( F in (Seq_of_ind (T | A)) . 0 iff B in (Seq_of_ind T) . 0 )
hence ( F in (Seq_of_ind (T | A)) . 0 iff B in (Seq_of_ind T) . 0 ) by A16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A1);
hence for F being Subset of (T | A) st F = B holds
( F in (Seq_of_ind (T | A)) . n iff B in (Seq_of_ind T) . n ) ; :: thesis: verum