set T = CofinTop X;
reconsider S = [#] X as Subset of () by Def6;
S is irreducible
proof
X = [#] () by Def6;
hence ( not S is empty & S is closed ) ; :: according to YELLOW_8:def 3 :: thesis: for S1, S2 being Subset of () st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S

let S1, S2 be Subset of (); :: thesis: ( S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S implies S2 = S )
assume that
A1: ( S1 is closed & S2 is closed ) and
A2: S = S1 \/ S2 ; :: thesis: ( S1 = S or S2 = S )
assume ( S1 <> S & S2 <> S ) ; :: thesis: contradiction
then reconsider S19 = S1, S29 = S2 as finite set by ;
S = S19 \/ S29 by A2;
hence contradiction ; :: thesis: verum
end;
then reconsider S = S as irreducible Subset of () ;
take S ; :: according to YELLOW_8:def 5 :: thesis: for p being Point of () holds
( not p is_dense_point_of S or ex q being Point of () st
( q is_dense_point_of S & not p = q ) )

let p be Point of (); :: thesis: ( not p is_dense_point_of S or ex q being Point of () st
( q is_dense_point_of S & not p = q ) )

now :: thesis: not p is_dense_point_of Send;
hence ( not p is_dense_point_of S or ex q being Point of () st
( q is_dense_point_of S & not p = q ) ) ; :: thesis: verum