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 A1, TOPS_3:77;

hence A is a_neighborhood of t by A2, A3, CONNSP_2:def 1; :: thesis: verum

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 A1, TOPS_3:77;

hence A is a_neighborhood of t by A2, A3, CONNSP_2:def 1; :: thesis: verum