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 by ORDINAL1:def 13;
( 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 ) ;
consider i being Element of n;
assume a: x `1 <> 0 ; :: thesis: contradiction
then A2: i in n ;
reconsider i = i as Element of NAT by a, ORDINAL1:19;
( n = varcl A & vars x c= Vars ) by A1, MCART_1:7;
then i in Vars by A2;
hence contradiction ; :: thesis: verum