theorem Th17: :: QC_LANG1:17

for A being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,A holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )