thus ( A is T_0 implies for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) ) :: thesis: ( ( for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) ) implies A is T_0 )
proof
assume A1: A is T_0 ; :: thesis: for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} )
let a be Point of X; :: thesis: ( a in A implies ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) )
assume A2: a in A ; :: thesis: ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} )
take D = MaxADSet a; :: thesis: ( D is maximal_anti-discrete & A /\ D = {a} )
thus D is maximal_anti-discrete by TEX_4:20; :: thesis: A /\ D = {a}
thus A /\ D = {a} by A1, A2; :: thesis: verum
end;
assume A3: for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete & A /\ D = {a} ) ; :: thesis: A is T_0
now :: thesis: for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a}
let a be Point of X; :: thesis: ( a in A implies A /\ (MaxADSet a) = {a} )
assume a in A ; :: thesis: A /\ (MaxADSet a) = {a}
then consider D being Subset of X such that
A4: D is maximal_anti-discrete and
A5: A /\ D = {a} by A3;
a in A /\ D by A5, ZFMISC_1:31;
then a in D by XBOOLE_0:def 4;
hence A /\ (MaxADSet a) = {a} by A4, A5, TEX_4:27; :: thesis: verum
end;
hence A is T_0 ; :: thesis: verum