let T be non empty Hausdorff TopSpace; :: thesis: T is sober

let S be irreducible Subset of T; :: according to YELLOW_8:def 5 :: thesis: ex p being Point of T st

( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds

p = q ) )

consider d being Element of S such that

A1: S = {d} by SUBSET_1:46;

reconsider d = d as Point of T ;

take d ; :: thesis: ( d is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds

d = q ) )

thus d is_dense_point_of S by A1, Th19; :: thesis: for q being Point of T st q is_dense_point_of S holds

d = q

let p be Point of T; :: thesis: ( p is_dense_point_of S implies d = p )

assume p is_dense_point_of S ; :: thesis: d = p

then p in S ;

hence d = p by A1, TARSKI:def 1; :: thesis: verum

let S be irreducible Subset of T; :: according to YELLOW_8:def 5 :: thesis: ex p being Point of T st

( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds

p = q ) )

consider d being Element of S such that

A1: S = {d} by SUBSET_1:46;

reconsider d = d as Point of T ;

take d ; :: thesis: ( d is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds

d = q ) )

thus d is_dense_point_of S by A1, Th19; :: thesis: for q being Point of T st q is_dense_point_of S holds

d = q

let p be Point of T; :: thesis: ( p is_dense_point_of S implies d = p )

assume p is_dense_point_of S ; :: thesis: d = p

then p in S ;

hence d = p by A1, TARSKI:def 1; :: thesis: verum