let n be Nat; :: thesis: ComplUniverse . n c= UNIVERSE (n + 1)
ComplUniverse . n = (UNIVERSE (n + 1)) \ (UNIVERSE n) by Def14;
hence ComplUniverse . n c= UNIVERSE (n + 1) ; :: thesis: verum