let x be Element of Vars ; :: thesis: ( vars x is natural implies vars x = 0 )
assume x `1 is natural ; :: thesis: vars x = 0
then reconsider n = x `1 as Element of NAT ;
( Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } & x in Vars ) by ABCMIZ_1:18;
then consider A being Subset of Vars, j being Element of NAT such that
A1: ( x = [(varcl A),j] & A is finite ) ;
set i = the Element of n;
assume A2: x `1 <> 0 ; :: thesis: contradiction
then A3: the Element of n in n ;
reconsider i = the Element of n as Element of NAT by A2, ORDINAL1:10;
( n = varcl A & vars x c= Vars ) by A1;
then i in Vars by A3;
hence contradiction ; :: thesis: verum