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
set d0 = the Element of D;
assume A1: ADTS D = 1TopSp D ; :: thesis: ex d0 being Element of D st D = {d0}
take the Element of D ; :: thesis: D = { the Element of D}
thus D = { the Element of D} 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:24; :: thesis: verum