let T be non empty TopSpace; :: thesis: for N being net of T
for p being Point of T st p in Lim N holds
for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let N be net of T; :: thesis: for p being Point of T st p in Lim N holds
for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let p be Point of T; :: thesis: ( p in Lim N implies for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J) )
assume A1: p in Lim N ; :: thesis: for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let J be net_set of the carrier of N,T; :: thesis: ( ( for i being Element of N holds N . i in Lim (J . i) ) implies p in Lim (Iterated J) )
assume A2: for i being Element of N holds N . i in Lim (J . i) ; :: thesis: p in Lim (Iterated J)
for V being a_neighborhood of p holds Iterated J is_eventually_in V

proof

let V be a_neighborhood of p; :: thesis: Iterated J is_eventually_in V
p in Int (Int V) by CONNSP_2:def 1;
then reconsider W = Int V as a_neighborhood of p by CONNSP_2:def 1;
N is_eventually_in W by A1, Def15;
then consider i being Element of N such that
A3: for j being Element of N st i <= j holds
N . j in W ;
defpred S₁[ Element of N, object ] means ex m being Element of (J . $1) st
( m = $2 & ( i <= $1 implies for n being Element of (J . $1) st m <= n holds
(J . $1) . n in W ) );
A4: Int V = Int (Int V) ;
A5: for j being Element of N ex e being object st S₁[j,e]

proof

let j be Element of N; :: thesis: ex e being object st S₁[j,e]
reconsider j9 = j as Element of N ;

per cases ( i <= j or not i <= j ) ;

suppose i <= j ; :: thesis: ex e being object st S₁[j,e]

then N . j9 in W by A3;
then A6: W is a_neighborhood of N . j by A4, CONNSP_2:def 1;
N . j in Lim (J . j) by A2;
then J . j is_eventually_in W by A6, Def15;
then consider e being Element of (J . j) such that
A7: for u being Element of (J . j) st e <= u holds
(J . j) . u in W ;
take e ; :: thesis: S₁[j,e]
take e ; :: thesis: ( e = e & ( i <= j implies for n being Element of (J . j) st e <= n holds
(J . j) . n in W ) )
thus e = e ; :: thesis: ( i <= j implies for n being Element of (J . j) st e <= n holds
(J . j) . n in W )
assume i <= j ; :: thesis: for n being Element of (J . j) st e <= n holds
(J . j) . n in W
thus for n being Element of (J . j) st e <= n holds
(J . j) . n in W by A7; :: thesis: verum

end;

suppose A8: not i <= j ; :: thesis: ex e being object st S₁[j,e]

set e = the Element of (J . j);
take the Element of (J . j) ; :: thesis: S₁[j, the Element of (J . j)]
take the Element of (J . j) ; :: thesis: ( the Element of (J . j) = the Element of (J . j) & ( i <= j implies for n being Element of (J . j) st the Element of (J . j) <= n holds
(J . j) . n in W ) )
thus ( the Element of (J . j) = the Element of (J . j) & ( i <= j implies for n being Element of (J . j) st the Element of (J . j) <= n holds
(J . j) . n in W ) ) by A8; :: thesis: verum

end;

end;

end;

consider f being ManySortedSet of the carrier of N such that
A9: for j being Element of N holds S₁[j,f . j] from PBOOLE:sch 6(A5);
A10: for x being object st x in dom (Carrier J) holds
f . x in (Carrier J) . x

proof

let x be object ; :: thesis: ( x in dom (Carrier J) implies f . x in (Carrier J) . x )
assume x in dom (Carrier J) ; :: thesis: f . x in (Carrier J) . x
then reconsider j = x as Element of N ;
ex m being Element of (J . j) st
( m = f . j & ( i <= j implies for n being Element of (J . j) st m <= n holds
(J . j) . n in W ) ) by A9;
then f . x in the carrier of (J . j) ;
hence f . x in (Carrier J) . x by Th2; :: thesis: verum

end;

dom (Carrier J) = the carrier of N by PARTFUN1:def 2;
then dom f = dom (Carrier J) by PARTFUN1:def 2;
then A11: f in product (Carrier J) by A10, CARD_3:9;
A12: the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):] by Th26;
then reconsider x = [i,f] as Element of (Iterated J) by A11, ZFMISC_1:87;
take x ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (Iterated J) holds
( not x <= b₁ or (Iterated J) . b₁ in V )
let j be Element of (Iterated J); :: thesis: ( not x <= j or (Iterated J) . j in V )
assume A13: x <= j ; :: thesis: (Iterated J) . j in V
consider j1 being Element of N, j2 being Element of product (Carrier J) such that
A14: j = [j1,j2] by A12, DOMAIN_1:1;
reconsider j2 = j2, i2 = f as Element of (product J) by A11, YELLOW_1:def 4;
reconsider i1 = i, j1 = j1 as Element of N ;
i2 in the carrier of (product J) ;
then A15: i2 in product (Carrier J) by YELLOW_1:def 4;
RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = [:N,(product J):] by Def13;
then A16: [i1,i2] <= [j1,j2] by A13, A14, YELLOW_0:1;
then i2 <= j2 by YELLOW_3:11;
then ex f, g being Function st
( f = i2 & g = j2 & ( for i being object st i in the carrier of N holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A15, YELLOW_1:def 4;
then A17: ex R being RelStr ex xi, yi being Element of R st
( R = J . j1 & xi = i2 . j1 & yi = j2 . j1 & xi <= yi ) ;
ex m being Element of (J . j1) st
( m = f . j1 & ( i <= j1 implies for n being Element of (J . j1) st m <= n holds
(J . j1) . n in W ) ) by A9;
then (J . j1) . (j2 . j1) in W by A16, A17, YELLOW_3:11;
then A18: (Iterated J) . j in W by A14, Th27;
W c= V by TOPS_1:16;
hence (Iterated J) . j in V by A18; :: thesis: verum

end;

hence p in Lim (Iterated J) by Def15; :: thesis: verum