let T1, T2 be non empty TopSpace; :: thesis:
assume A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) ; :: thesis:
let N1 be net of T1; :: thesis:
let N2 be net of T2; :: thesis:
assume A2: N1 = N2 ; :: thesis:
let p1 be Point of T1; :: thesis:
let p2 be Point of T2; :: thesis:
assume that
A3: p1 = p2 and
A4: p1 in Lim N1 ; :: thesis:
for V being a_neighborhood of p2 holds N2 is_eventually_in V

let V be a_neighborhood of p2; :: thesis:
reconsider W = V as Subset of T1 by A1;
p2 in Int V by CONNSP_2:def 1;
then consider G being Subset of T2 such that
A5: G is open and
A6: G c= V and
A7: p2 in G by TOPS_1:22;
reconsider H = G as Subset of T1 by A1;
G in the topology of T2 by A5;
then H is open by A1;
then p1 in Int W by A3, A6, A7, TOPS_1:22;
then reconsider W = V as a_neighborhood of p1 by CONNSP_2:def 1;
thus N2 is_eventually_in V :: thesis:

N1 is_eventually_in W by A4, YELLOW_6:def 15;
then consider i being Element of N1 such that
A8: for j being Element of N1 st i <= j holds
N1 . j in W ;
reconsider ii = i as Element of N2 by A2;
take ii ; :: according to WAYBEL_0:def 11 :: thesis:
let jj be Element of N2; :: thesis:
reconsider j = jj as Element of N1 by A2;
assume A9: ii <= jj ; :: thesis:
N2 . jj = N1 . j by A2;
hence N2 . jj in V by A2, A8, A9; :: thesis:

end;