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

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

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

{} ({} -DiscreteTop X) = {}
;
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;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

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