:: deftheorem Def2 defines Vars ABCMIZ_1:def 2 :
for b₁ being set holds
( b₁ = Vars iff ex V being ManySortedSet of NAT st
( b₁ = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) );