set x = 5 + n;
5 <= 5 + n by NAT_1:11;
then 5 + n in { k where k is Element of NAT : 5 <= k } ;
hence 5 + n is Variable ; :: thesis: verum