let S, T be non empty TopSpace; :: thesis: for s being Point of S
for t being Point of T
for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds
A is a_neighborhood of t

let s be Point of S; :: thesis: for t being Point of T
for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds
A is a_neighborhood of t

let t be Point of T; :: thesis: for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds
A is a_neighborhood of t

let A be a_neighborhood of s; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t implies A is a_neighborhood of t )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: s = t ; :: thesis: A is a_neighborhood of t
reconsider B = A as Subset of T by A1;
A3: s in Int A by CONNSP_2:def 1;
Int A = Int B by ;
hence A is a_neighborhood of t by ; :: thesis: verum