:: deftheorem Def14 defines ComplUniverse CLASSES4:def 14 :
for b₁ being Function of NAT,(union (rng sequence_univers)) holds
( b₁ = ComplUniverse iff for n being Nat holds b₁ . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) );