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

set d1 = the Element of D \ {d0};
assume A1: STS (D,d0) = ADTS D ; :: thesis:
assume A2: D <> {d0} ; :: thesis:

end;

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

end;