theorem Th31: :: GOEDELCP:31

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is with_examples )