set T = CofinTop X;

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

S is irreducible

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 ) )

( q is_dense_point_of S & not p = q ) ) ; :: thesis: verum

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

S is irreducible

proof

then reconsider S = S as irreducible Subset of (CofinTop X) ;
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;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

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

hence
( not p is_dense_point_of S or ex q being Point of (CofinTop X) st 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;then S c= Cl {p} ;

then Cl {p} is infinite ;

hence contradiction by Th26; :: thesis: verum

( q is_dense_point_of S & not p = q ) ) ; :: thesis: verum