card X = card (FreeGenSetNSG (ECIW-signature,X)) by Th70;
then not card (ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X))) is finite by Th70;
hence not ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) is finite ; :: according to AOFA_000:def 23 :: thesis: verum