let X be non empty TopSpace; :: thesis: for A being Subset of X st ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) holds
A is discrete
let A be Subset of X; :: thesis: ( ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) implies A is discrete )
assume A1: for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ; :: thesis: A is discrete

hereby :: thesis: verum

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: A is discrete

hence A is discrete by Th35; :: thesis: verum

end;

suppose not A is empty ; :: thesis: A is discrete

then consider X0 being non empty strict SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
A3: [#] X = the carrier of X ;
[#] X0 = the carrier of X0 ;
then A4: the carrier of X0 c= the carrier of X by A3, PRE_TOPC:def 9;

now

let C be Subset of X0; :: thesis: for y being Point of X0 st C = {y} holds
C is open
let y be Point of X0; :: thesis: ( C = {y} implies C is open )
reconsider x = y as Point of X by A4, TARSKI:def 3;
consider G being Subset of X such that
A5: G is open and
A6: A /\ G = {x} by A1, A2;
assume A7: C = {y} ; :: thesis: C is open

now

take G = G; :: thesis: ( G in the topology of X & G /\ ([#] X0) = C )
thus G in the topology of X by A5, PRE_TOPC:def 5; :: thesis: G /\ ([#] X0) = C
thus G /\ ([#] X0) = C by A2, A7, A6; :: thesis: verum

end;

then C in the topology of X0 by PRE_TOPC:def 9;
hence C is open by PRE_TOPC:def 5; :: thesis: verum

end;

then X0 is discrete by TDLAT_3:19;
hence A is discrete by A2, Th26; :: thesis: verum

end;

end;

end;