let T be non empty Hausdorff TopSpace; :: thesis: for S being irreducible Subset of T holds S is trivial
let S be irreducible Subset of T; :: thesis: S is trivial
assume not S is trivial ; :: thesis: contradiction
then consider x, y being Element of S such that
A1: x <> y by Def1;
reconsider x = x, y = y as Point of T ;
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 16;
A5: S is closed by Def4;
set S1 = S \ W;
set S2 = S \ V;
A6: ( S \ W is closed & S \ V is closed ) by A2, A5, Th29;
A7: W /\ V = {} by A4, XBOOLE_0:def 7;
A8: (S \ W) \/ (S \ V) = S \ (W /\ V) by XBOOLE_1:54
.= S by A7 ;
( S \ W <> S & S \ V <> S ) by A3, XBOOLE_0:def 5;
hence contradiction by A6, A8, Def4; :: thesis: verum