let X be set ; :: thesis: X in (Seq_of_ind (1TopSp X)) . 1
set T = 1TopSp X;
set CT = [#] (1TopSp X);

now :: thesis: for p being Point of ((1TopSp X) | ([#] (1TopSp X)))
for U being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st p in U holds
ex W being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st
( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 )

let p be Point of ((1TopSp X) | ([#] (1TopSp X))); :: thesis: for U being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st p in U holds
ex W being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st
( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 )
let U be open Subset of ((1TopSp X) | ([#] (1TopSp X))); :: thesis: ( p in U implies ex W being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st
( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 ) )
assume A1: p in U ; :: thesis: ex W being open Subset of ((1TopSp X) | ([#] (1TopSp X))) st
( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 )
take W = U; :: thesis: ( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 )
A2: [#] ((1TopSp X) | ([#] (1TopSp X))) = [#] (1TopSp X) by PRE_TOPC:def 5;
then reconsider W9 = U as Subset of (1TopSp X) ;
W9 ` is open by PRE_TOPC:def 2;
then ( W9 is open & W9 is closed ) by PRE_TOPC:def 2, TOPS_1:3;
then Fr W9 = {} (1TopSp X) by TOPGEN_1:14;
then A3: (Fr W9) /\ ([#] (1TopSp X)) = {} ;
W = W /\ ([#] (1TopSp X)) by A2, XBOOLE_1:28;
then Fr W c= {} (1TopSp X) by A3, Th1;
then A4: Fr W = {} (1TopSp X) ;
(Seq_of_ind (1TopSp X)) . 0 = {({} (1TopSp X))} by Def1;
hence ( p in W & W c= U & Fr W in (Seq_of_ind (1TopSp X)) . 0 ) by A1, A4, TARSKI:def 1; :: thesis: verum

end;

then [#] (1TopSp X) in (Seq_of_ind (1TopSp X)) . (0 + 1) by Def1;
hence X in (Seq_of_ind (1TopSp X)) . 1 ; :: thesis: verum