let n be Nat; :: thesis: not (UNIVERSE (n + 1)) \ (UNIVERSE n) in UNIVERSE (n + 1)
UNIVERSE n is Element of UNIVERSE (n + 1) by Th99;
hence not (UNIVERSE (n + 1)) \ (UNIVERSE n) in UNIVERSE (n + 1) by Th86; :: thesis: verum