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] & A is finite ) by Th16;
( varcl {x} = (varcl A) \/ {x} & vars x = varcl A & i in NAT ) by A1, Lem8, MCART_1:7, ORDINAL1:def 13;
hence [((vars x) \/ {x}),i] in Vars by Th16; :: thesis: verum