Metamath Proof Explorer


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 Top
kur14lem.x X = J
kur14lem.k K = cls J
kur14lem.i I = int J
kur14lem.a A X
Assertion kur14lem4 X X A = A

Proof

Step Hyp Ref Expression
1 kur14lem.j J Top
2 kur14lem.x X = J
3 kur14lem.k K = cls J
4 kur14lem.i I = int J
5 kur14lem.a A X
6 dfss4 A X X X A = A
7 5 6 mpbi X X A = A