theorem Th70: :: AOFA_000:70

for X being non empty disjoint_with_NAT set holds
( ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) = FreeGenSetNSG (ECIW-signature,X) & card X = card (FreeGenSetNSG (ECIW-signature,X)) )