let X be non empty discrete TopSpace; :: thesis: for A being Subset of X holds
( Cl A = A & Int A = A )
let A be Subset of X; :: thesis: ( Cl A = A & Int A = A )
reconsider B = A as Subset of X ;
( B is open & B is closed ) by TDLAT_3:17, TDLAT_3:18;
hence ( Cl A = A & Int A = A ) by PRE_TOPC:52, TOPS_1:55; :: thesis: verum