let T be non empty TopSpace; :: thesis: ( not T is T_1 implies ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} ) )
assume not T is T_1 ; :: thesis: ex x1, x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )
then consider x1 being Point of T such that
A1: Cl {x1} <> {x1} by Lm1;
( not {x1} c= Cl {x1} or not Cl {x1} c= {x1} ) by A1;
then consider x2 being object such that
A2: x2 in Cl {x1} and
A3: not x2 in {x1} by PRE_TOPC:18;
reconsider x2 = x2 as Point of T by A2;
take x1 ; :: thesis: ex x2 being Point of T st
( x1 <> x2 & x2 in Cl {x1} )
take x2 ; :: thesis: ( x1 <> x2 & x2 in Cl {x1} )
thus x1 <> x2 by A3, TARSKI:def 1; :: thesis: x2 in Cl {x1}
thus x2 in Cl {x1} by A2; :: thesis: verum