let S, T be non empty TopSpace; :: thesis: for a being Point of S
for b being Point of T
for A being Subset of S
for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
let a be Point of S; :: thesis: for b being Point of T
for A being Subset of S
for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
let b be Point of T; :: thesis: for A being Subset of S
for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
let A be Subset of S; :: thesis: for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
let B be Subset of T; :: thesis: ( a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A implies b is_dense_point_of B )
assume ( a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a in A & A c= Cl {a} ) ; :: according to YELLOW_8:def 4 :: thesis: b is_dense_point_of B
hence ( b in B & B c= Cl {b} ) by TOPS_3:80; :: according to YELLOW_8:def 4 :: thesis: verum