theorem Th88: :: CLASSES4:88

for X being set ex f being Function st
( dom f = NAT & f . 0 = X & ( for n being Nat holds f . (n + 1) = GrothendieckUniverse (f . n) ) )