let n be Nat; :: thesis: not ComplUniverse . n is empty
assume ComplUniverse . n is empty ; :: thesis: contradiction
then A1: (UNIVERSE (n + 1)) \ (UNIVERSE n) = {} by Def14;
A2: UNIVERSE (n + 1) is axiom_GU1 ;
UNIVERSE n in UNIVERSE (n + 1) by Th99;
then UNIVERSE n c= UNIVERSE (n + 1) by A2;
then UNIVERSE (n + 1) = UNIVERSE n by A1, XBOOLE_1:37;
then n = n + 1 by CLASSES2:71;
hence contradiction ; :: thesis: verum