P in { [k,x] where k is Nat, x is QC-symbol of A : 7 <= k } ;
then consider k being Nat, x being QC-symbol of A such that
A1: P = [k,x] and
A2: 7 <= k ;
consider w being Nat such that
A3: k = 7 + w by A2, NAT_1:10;
thus ex b₁ being Nat st P `1 = 7 + b₁ by A1, A3; :: thesis: verum