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 | ||
kur14lem.x | |||
kur14lem.k | |||
kur14lem.i | |||
kur14lem.a | |||
Assertion | kur14lem4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | kur14lem.j | ||
2 | kur14lem.x | ||
3 | kur14lem.k | ||
4 | kur14lem.i | ||
5 | kur14lem.a | ||
6 | dfss4 | ||
7 | 5 6 | mpbi |