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 ;
A1: B is closed by TDLAT_3:18;
B is open by TDLAT_3:17;
hence ( Cl A = A & Int A = A ) by A1, PRE_TOPC:52, TOPS_1:55; :: thesis: verum