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 S ex a being Point of S st
( a is_dense_point_of A & ( for b being Point of S st b is_dense_point_of A holds
a = b ) ) ; :: according to YELLOW_8:def 5 :: thesis: T is sober
let B be irreducible Subset of T; :: according to YELLOW_8:def 5 :: 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 S by A1, Th23;
consider a being Point of S such that
A3: a is_dense_point_of A and
A4: for b being Point of S st b is_dense_point_of A holds
a = b by A2;
reconsider p = a as Point of T 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, Th24; :: 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 T; :: thesis: ( not q is_dense_point_of B or p = q )
reconsider b = q as Point of S by A1;
assume q is_dense_point_of B ; :: thesis: p = q
then b is_dense_point_of A by A1, Th24;
hence p = q by A4; :: thesis: verum