theorem :: CLASSES4:97

for X being set
for n being Nat holds
( (sequence_univers X) . (n + 1) is epsilon-transitive & Tarski-Class ((sequence_univers X) . (n + 1)) = GrothendieckUniverse ((sequence_univers X) . (n + 1)) )