Theorem kur14lem4

Description: Lemma for kur14 . Complementation is an involution on the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	kur14lem.j	$$⊢J\in \mathrm{Top}$$
	kur14lem.x	$$⊢X=\bigcup J$$
	kur14lem.k	$$⊢K=\mathrm{cls}\left(J\right)$$
	kur14lem.i	$$⊢I=\mathrm{int}\left(J\right)$$
	kur14lem.a	$$⊢A\subseteq X$$
Assertion	kur14lem4	$$⊢X\setminus \left(X\setminus A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		kur14lem.j	$$⊢J\in \mathrm{Top}$$
2		kur14lem.x	$$⊢X=\bigcup J$$
3		kur14lem.k	$$⊢K=\mathrm{cls}\left(J\right)$$
4		kur14lem.i	$$⊢I=\mathrm{int}\left(J\right)$$
5		kur14lem.a	$$⊢A\subseteq X$$
6		dfss4	$$⊢A\subseteq X\leftrightarrow X\setminus \left(X\setminus A\right)=A$$
7	5 6	mpbi	$$⊢X\setminus \left(X\setminus A\right)=A$$