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