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 JTop
kur14lem.x X=J
kur14lem.k K=clsJ
kur14lem.i I=intJ
kur14lem.a AX
Assertion kur14lem4 XXA=A

Proof

Step Hyp Ref Expression
1 kur14lem.j JTop
2 kur14lem.x X=J
3 kur14lem.k K=clsJ
4 kur14lem.i I=intJ
5 kur14lem.a AX
6 dfss4 AXXXA=A
7 5 6 mpbi XXA=A