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 )
consider a being object such that
A1: a in A by XBOOLE_0:def 1;
reconsider a = a as Point of X by A1;
assume A is discrete ; :: thesis: A is trivial
then consider G being Subset of X such that
A2: G is open and
A3: A /\ G = {a} by A1, Th26;
G <> {} by A3;
then A4: G = the carrier of X by A2, TDLAT_3:18;
now :: thesis: ex a being Point of X st A = {a}
take a = a; :: thesis: A = {a}
thus A = {a} by A3, A4, 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 ex a being Element of A st A = {a} by SUBSET_1:46;
hence A is discrete by Th30; :: thesis: verum
end;