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