0 is QC-symbol of A by Th3;
then [7,0] in { [n,x] where n is Nat, x is QC-symbol of A : 7 <= n } ;
hence not QC-pred_symbols A is empty ; :: thesis: verum