let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
let P be QC-pred_symbol of k; :: thesis: ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
reconsider P9 = P as QC-pred_symbol ;
P9 `1 = 7 + (the_arity_of P9) by Def6;
hence ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 ) by NAT_1:11; :: thesis: verum