let X, x0 be set ; :: thesis: for A being Subset of (DiscrWithInfin X,x0) st A ` is finite holds
Int A = A
let A be Subset of (DiscrWithInfin X,x0); :: thesis: ( A ` is finite implies Int A = A )
assume A ` is finite ; :: thesis: Int A = A
then Cl (A ` ) = A ` by Th26;
hence Int A = (A ` ) ` by TOPS_1:def 1
.= A ;
:: thesis: verum