reconsider C = {} as Chain of W by Th19;
take C ; :: thesis: C is finite
thus C is finite ; :: thesis: verum