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 e. Top
	kur14lem.x	|- X = U. J
	kur14lem.k	|- K = ( cls ` J )
	kur14lem.i	|- I = ( int ` J )
	kur14lem.a	|- A C_ X
Assertion	kur14lem4	|- ( X \ ( X \ A ) ) = A

Proof

Step	Hyp	Ref	Expression
1		kur14lem.j	|- J e. Top
2		kur14lem.x	|- X = U. J
3		kur14lem.k	|- K = ( cls ` J )
4		kur14lem.i	|- I = ( int ` J )
5		kur14lem.a	|- A C_ X
6		dfss4	|- ( A C_ X <-> ( X \ ( X \ A ) ) = A )
7	5 6	mpbi	|- ( X \ ( X \ A ) ) = A