let D be non empty set ; :: thesis: ( ADTS D = 1TopSp D iff ex d0 being Element of D st D = {d0} )
thus ( ADTS D = 1TopSp D implies ex d0 being Element of D st D = {d0} ) :: thesis: ( ex d0 being Element of D st D = {d0} implies ADTS D = 1TopSp D )

proof

consider d0 being Element of D;
assume A1: ADTS D = 1TopSp D ; :: thesis: ex d0 being Element of D st D = {d0}
take d0 ; :: thesis: D = {d0}
thus D = {d0} by A1, TARSKI:def 2; :: thesis: verum

end;

given d0 being Element of D such that A2: D = {d0} ; :: thesis: ADTS D = 1TopSp D
thus ADTS D = 1TopSp D by A2, ZFMISC_1:30; :: thesis: verum