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: the topology of ({} -DiscreteTop X) c= cobool X
proof
let a be object ; :: 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;
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;
hence a in cobool X by A2, TARSKI:def 2; :: thesis: verum
end;
{} ({} -DiscreteTop X) = {} ;
then A5: {} in the topology of ({} -DiscreteTop X) by PRE_TOPC:def 2;
[#] ({} -DiscreteTop X) = X by Def8;
then X in the topology of ({} -DiscreteTop X) by PRE_TOPC:def 2;
then cobool X c= the topology of ({} -DiscreteTop X) by A5, A2, ZFMISC_1:32;
then the topology of ({} -DiscreteTop X) = cobool X by A3;
hence ADTS X = {} -DiscreteTop X by A1, TEX_1:def 3; :: thesis: verum