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

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

A3: now :: thesis: not D \ {d0} = {}

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

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: 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:24; :: thesis: verum