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

X = [#] (CofinTop X) by Def6;
hence ( not S is empty & S is closed ) ; :: according to YELLOW_8:def 3 :: thesis:
let S1, S2 be Subset of (CofinTop X); :: thesis:
assume that
A1: ( S1 is closed & S2 is closed ) and
A2: S = S1 \/ S2 ; :: thesis:
assume ( S1 <> S & S2 <> S ) ; :: thesis:
then reconsider S19 = S1, S29 = S2 as finite set by A1, Th25;
S = S19 \/ S29 by A2;
hence contradiction ; :: thesis:

end;

then reconsider S = S as irreducible Subset of (CofinTop X) ;
take S ; :: according to YELLOW_8:def 5 :: thesis:
let p be Point of (CofinTop X); :: thesis:

end;