v1 in VAR
;
then consider k being Element of NAT such that
A1:
v1 = k
and
A2:
k >= 5
by ZF_LANG:def 1;
consider m being Nat such that
A3:
k = 5 + m
by A2, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take
m
; x. m = v1
thus
x. m = v1
by A1, A3, ZF_LANG:def 2; verum