:: deftheorem Def9 defines sequence_univers CLASSES4:def 9 :
for X being set
for b₂ being Function holds
( b₂ = sequence_univers X iff ( dom b₂ = NAT & b₂ . 0 = X & ( for n being Nat holds b₂ . (n + 1) = GrothendieckUniverse (b₂ . n) ) ) );