let S, T be non empty TopSpace; :: thesis: ( TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) & S is sober implies T is sober )
assume that
A1: TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) and
A2: for A being irreducible Subset of ex a being Point of st
( a is_dense_point_of A & ( for b being Point of st b is_dense_point_of A holds
a = b ) ) ; :: according to YELLOW_8:def 6 :: thesis: T is sober
let B be irreducible Subset of ; :: according to YELLOW_8:def 6 :: thesis: ex b₁ being Element of the carrier of T st
( b₁ is_dense_point_of B & ( for b₂ being Element of the carrier of T holds
( not b₂ is_dense_point_of B or b₁ = b₂ ) ) )
reconsider A = B as irreducible Subset of by A1, Th24;
consider a being Point of such that
A3: a is_dense_point_of A and
A4: for b being Point of st b is_dense_point_of A holds
a = b by A2;
reconsider p = a as Point of by A1;
take p ; :: thesis: ( p is_dense_point_of B & ( for b₁ being Element of the carrier of T holds
( not b₁ is_dense_point_of B or p = b₁ ) ) )
thus p is_dense_point_of B by A1, A3, Th25; :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ is_dense_point_of B or p = b₁ )
let q be Point of ; :: thesis: ( not q is_dense_point_of B or p = q )
reconsider b = q as Point of by A1;
assume q is_dense_point_of B ; :: thesis: p = q
then b is_dense_point_of A by A1, Th25;
hence p = q by A4; :: thesis: verum