let S, T be non empty TopSpace; :: thesis: for A being Subset of S

for B being Subset of T

for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds

N is a_neighborhood of B

let A be Subset of S; :: thesis: for B being Subset of T

for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds

N is a_neighborhood of B

let B be Subset of T; :: thesis: for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds

N is a_neighborhood of B

let N be a_neighborhood of A; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B implies N is a_neighborhood of B )

assume that

A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and

A2: A = B ; :: thesis: N is a_neighborhood of B

reconsider M = N as Subset of T by A1;

A3: A c= Int N by CONNSP_2:def 2;

Int M = Int N by A1, TOPS_3:77;

hence N is a_neighborhood of B by A2, A3, CONNSP_2:def 2; :: thesis: verum

for B being Subset of T

for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds

N is a_neighborhood of B

let A be Subset of S; :: thesis: for B being Subset of T

for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds

N is a_neighborhood of B

let B be Subset of T; :: thesis: for N being a_neighborhood of A st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B holds

N is a_neighborhood of B

let N be a_neighborhood of A; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A = B implies N is a_neighborhood of B )

assume that

A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and

A2: A = B ; :: thesis: N is a_neighborhood of B

reconsider M = N as Subset of T by A1;

A3: A c= Int N by CONNSP_2:def 2;

Int M = Int N by A1, TOPS_3:77;

hence N is a_neighborhood of B by A2, A3, CONNSP_2:def 2; :: thesis: verum