set T = CofinTop X;
reconsider S = [#] X as Subset of (CofinTop X) by Def6;
S is irreducible

proof

X = [#] (CofinTop X) by Def6;
hence ( not S is empty & S is closed ) ; :: according to YELLOW_8:def 3 :: thesis: for S1, S2 being Subset of (CofinTop X) st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S
let S1, S2 be Subset of (CofinTop X); :: 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 A1, Th25;
S = S19 \/ S29 by A2;
hence contradiction ; :: thesis: verum

end;

then reconsider S = S as irreducible Subset of (CofinTop X) ;
take S ; :: according to YELLOW_8:def 5 :: thesis: for p being Point of (CofinTop X) holds
( not p is_dense_point_of S or ex q being Point of (CofinTop X) st
( q is_dense_point_of S & not p = q ) )
let p be Point of (CofinTop X); :: thesis: ( not p is_dense_point_of S or ex q being Point of (CofinTop X) st
( q is_dense_point_of S & not p = q ) )

now :: thesis: not p is_dense_point_of S

assume p is_dense_point_of S ; :: thesis: contradiction
then S c= Cl {p} ;
then Cl {p} is infinite ;
hence contradiction by Th26; :: thesis: verum

end;

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