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