let D be non empty set ; :: thesis: for d0 being Element of D holds
( STS D,d0 = ADTS D iff D = {d0} )
let d0 be Element of D; :: thesis: ( STS D,d0 = ADTS D iff D = {d0} )
set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ;
thus ( STS D,d0 = ADTS D implies D = {d0} ) :: thesis: ( D = {d0} implies STS D,d0 = ADTS D )

proof

assume A1: STS D,d0 = ADTS D ; :: thesis: D = {d0}
assume A2: D <> {d0} ; :: thesis: contradiction
A3: {d0} c= D ;

A4: now

assume D \ {d0} = {} ; :: thesis: contradiction
then D c= {d0} by XBOOLE_1:37;
hence contradiction by A2, XBOOLE_0:def 10; :: thesis: verum

end;

consider d1 being Element of D \ {d0};
reconsider d1 = d1 as Element of D by A4, XBOOLE_0:def 5;
A5: d0 <> d1 by A4, ZFMISC_1:64;
reconsider P = {d1} as Subset of D ;
for Q being Subset of D holds
( not Q = P or not d0 in Q or not Q <> D ) by A5, TARSKI:def 1;
then not P in { P where P is Subset of D : ( d0 in P & P <> D ) } ;
then P in {{} ,D} by A1, XBOOLE_0:def 5;
then {d0} c= {d1} by A3, TARSKI:def 2;
hence contradiction by A5, ZFMISC_1:24; :: thesis: verum

end;

assume A6: D = {d0} ; :: thesis: STS D,d0 = ADTS D
then { P where P is Subset of D : ( d0 in P & P <> D ) } = {} by Lm2;
hence STS D,d0 = ADTS D by A6, ZFMISC_1:30; :: thesis: verum