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: Int A = Int B by A1, TOPS_3:77;
s in Int A by CONNSP_2:def 1;
hence A is a_neighborhood of t by A2, A3, CONNSP_2:def 1; :: thesis: verum