theorem Th14: :: ABCMIZ_1:14

for V being ManySortedSet of NAT st 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 } ) holds
for i, j being Element of NAT st i <= j holds
V . i c= V . j