P in { [k,l] where k, l is Element of NAT : 7 <= k } ;
then consider k, l being Element of NAT such that
A1: P = [k,l] and
A2: 7 <= k ;
consider w being Nat such that
A3: k = 7 + w by A2, NAT_1:10;
w in NAT by ORDINAL1:def 12;
hence ex b₁ being Element of NAT st P `1 = 7 + b₁ by A1, A3, MCART_1:7; :: thesis: verum