let x be Element of Vars ; :: thesis: x is pair
( 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 ex A being Subset of Vars ex j being Element of NAT st
( x = [(varcl A),j] & A is finite ) ;
hence x is pair ; :: thesis: verum