let S, T be non empty TopSpace; :: thesis: for a being Point of
for b being Point of
for A being Subset of
for B being Subset of 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 ; :: thesis: for b being Point of
for A being Subset of
for B being Subset of 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 ; :: thesis: for A being Subset of
for B being Subset of 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 ; :: thesis: for B being Subset of 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 ; :: 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 5 :: thesis: b is_dense_point_of B
hence ( b in B & B c= Cl {b} ) by TOPS_3:80; :: according to YELLOW_8:def 5 :: thesis: verum