Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set C . (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | disjinfi.b | |
|
disjinfi.d | |
||
disjinfi.c | |
||
Assertion | disjinfi | |