let X be non empty anti-discrete TopSpace; :: thesis: for A being non empty Subset of X holds
( A is discrete iff A is trivial )
let A be non empty Subset of X; :: thesis: ( A is discrete iff A is trivial )

hereby :: thesis: ( A is trivial implies A is discrete )

assume A1: A is discrete ; :: thesis: A is trivial
consider a being set such that
A2: a in A by XBOOLE_0:def 1;
reconsider a = a as Point of X by A2;
consider G being Subset of X such that
A3: G is open and
A4: A /\ G = {a} by A1, A2, Th32;
G <> {} by A4;
then A5: G = the carrier of X by A3, TDLAT_3:20;

now

take a = a; :: thesis: A = {a}
thus A = {a} by A4, A5, XBOOLE_1:28; :: thesis: verum

end;

hence A is trivial ; :: thesis: verum

end;

hereby :: thesis: verum

assume A is trivial ; :: thesis: A is discrete
then consider a being Element of A such that
A6: A = {a} by Def1;
thus A is discrete by A6, Th36; :: thesis: verum

end;