reconsider E = {} as Element of C by COH_SP:1;
take E ; :: thesis: E is finite
thus E is finite ; :: thesis: verum