let T be non empty TopSpace; :: thesis: for p being Point of T holds Cl {p} is irreducible

let p be Point of T; :: thesis: Cl {p} is irreducible

assume A1: not Cl {p} is irreducible ; :: thesis: contradiction

not Cl {p} is empty by PCOMPS_1:2;

then consider S1, S2 being Subset of T such that

A2: ( S1 is closed & S2 is closed ) and

A3: Cl {p} = S1 \/ S2 and

A4: ( S1 <> Cl {p} & S2 <> Cl {p} ) by A1;

( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def 1;

then ( p in S1 or p in S2 ) by A3, XBOOLE_0:def 3;

then ( {p} c= S1 or {p} c= S2 ) by ZFMISC_1:31;

then A5: ( Cl {p} c= S1 or Cl {p} c= S2 ) by A2, TOPS_1:5;

( S1 c= Cl {p} & S2 c= Cl {p} ) by A3, XBOOLE_1:7;

hence contradiction by A4, A5; :: thesis: verum

let p be Point of T; :: thesis: Cl {p} is irreducible

assume A1: not Cl {p} is irreducible ; :: thesis: contradiction

not Cl {p} is empty by PCOMPS_1:2;

then consider S1, S2 being Subset of T such that

A2: ( S1 is closed & S2 is closed ) and

A3: Cl {p} = S1 \/ S2 and

A4: ( S1 <> Cl {p} & S2 <> Cl {p} ) by A1;

( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def 1;

then ( p in S1 or p in S2 ) by A3, XBOOLE_0:def 3;

then ( {p} c= S1 or {p} c= S2 ) by ZFMISC_1:31;

then A5: ( Cl {p} c= S1 or Cl {p} c= S2 ) by A2, TOPS_1:5;

( S1 c= Cl {p} & S2 c= Cl {p} ) by A3, XBOOLE_1:7;

hence contradiction by A4, A5; :: thesis: verum