theorem :: CLASSES4:106

for X being Element of union (rng sequence_univers)
for n being Nat st rank_univers X <= n holds
X in sequence_univers . n