let X be non empty discrete TopSpace; :: thesis: for A being Subset of holds
( Cl A = A & Int A = A )
let A be Subset of ; :: thesis: ( Cl A = A & Int A = A )
reconsider B = A as Subset of ;
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