let T be non empty Hausdorff TopSpace; for S being irreducible Subset of T holds S is trivial
let S be irreducible Subset of T; S is trivial
assume
not S is trivial
; contradiction
then consider x, y being Point of T such that
A1:
( x in S & y in S )
and
A2:
x <> y
by SUBSET_1:45;
consider W, V being Subset of T such that
A3:
( W is open & V is open )
and
A4:
( x in W & y in V )
and
A5:
W misses V
by A2, PRE_TOPC:def 10;
set S1 = S \ W;
set S2 = S \ V;
A6:
( S \ W <> S & S \ V <> S )
by A4, A1, XBOOLE_0:def 5;
S is closed
by Def3;
then A7:
( S \ W is closed & S \ V is closed )
by A3, Th20;
A8:
W /\ V = {}
by A5;
(S \ W) \/ (S \ V) =
S \ (W /\ V)
by XBOOLE_1:54
.=
S
by A8
;
hence
contradiction
by A7, A6, Def3; verum