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
B1:
( x in S & y in S )
and
A1:
x <> y
by SUBSET_1:45;
consider W, V being Subset of T such that
A2:
( W is open & V is open )
and
A3:
( x in W & y in V )
and
A4:
W misses V
by A1, PRE_TOPC:def 10;
set S1 = S \ W;
set S2 = S \ V;
A5:
( S \ W <> S & S \ V <> S )
by A3, B1, XBOOLE_0:def 5;
S is closed
by Def4;
then A6:
( S \ W is closed & S \ V is closed )
by A2, Th29;
A7:
W /\ V = {}
by A4, XBOOLE_0:def 7;
(S \ W) \/ (S \ V) =
S \ (W /\ V)
by XBOOLE_1:54
.=
S
by A7
;
hence
contradiction
by A6, A5, Def4; verum