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 & 5 <= j ) ;
consider i being Nat such that
A2: j = 5 + i by A1, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
take i ; :: thesis: x = x. i
thus x = x. i by A1, A2; :: thesis: verum