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 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; :: thesis: verum

let S be irreducible Subset of T; :: thesis: S is trivial

assume not S is trivial ; :: thesis: 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; :: thesis: verum