let x be Variable; :: thesis: ex i being Element of NAT st x = x. i
x in VAR ;
then consider j being Element of NAT such that
A1: x = j and
A2: 5 <= j ;
consider i being Nat such that
A3: j = 5 + i by A2, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
take i ; :: thesis: x = x. i
thus x = x. i by A1, A3; :: thesis: verum