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 Th24;
hence Int A = (A `) ` by TOPS_1:def 1
.= A ;
:: thesis: verum