let i be Nat; :: thesis: for x being variable holds [((vars x) \/ {x}),i] in Vars
let x be variable; :: thesis: [((vars x) \/ {x}),i] in Vars
x in Vars ;
then consider A being Subset of Vars, j being Element of NAT such that
A1: x = [(varcl A),j] and
A is finite by Th18;
A2: varcl {x} = (varcl A) \/ {x} by A1, Th26;
A3: vars x = varcl A by A1;
i in NAT by ORDINAL1:def 12;
hence [((vars x) \/ {x}),i] in Vars by A2, A3, Th18; :: thesis: verum