let X be set ; :: thesis: ADTS X = {} -DiscreteTop X
set T = {} -DiscreteTop X;
A1: the carrier of ({} -DiscreteTop X) = X by Def8;
A2: cobool X = {{} ,X} by TEX_1:def 2;
A3: ( {} ({} -DiscreteTop X) = {} & [#] ({} -DiscreteTop X) = X ) by Def8;
the topology of ({} -DiscreteTop X) = cobool X

proof

thus the topology of ({} -DiscreteTop X) c= cobool X :: according to XBOOLE_0:def 10 :: thesis: cobool X c= the topology of ({} -DiscreteTop X)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the topology of ({} -DiscreteTop X) or a in cobool X )
assume A4: a in the topology of ({} -DiscreteTop X) ; :: thesis: a in cobool X
then reconsider a = a as Subset of ({} -DiscreteTop X) ;
a is open by A4, PRE_TOPC:def 5;
then ( ( a c= X & X is empty ) or not a is proper or a c= {} ) by A1, Th43;
then ( a = {} or a = X ) by A1, SUBSET_1:def 7;
hence a in cobool X by A2, TARSKI:def 2; :: thesis: verum

end;

( {} in the topology of ({} -DiscreteTop X) & X in the topology of ({} -DiscreteTop X) ) by A3, PRE_TOPC:def 5;
hence cobool X c= the topology of ({} -DiscreteTop X) by A2, ZFMISC_1:38; :: thesis: verum

end;

hence ADTS X = {} -DiscreteTop X by A1, TEX_1:def 3; :: thesis: verum