CLASSES4

:: Non-trivial Universes and Sequences of Universes
::  by Roland Coghetto
:: 
:: Received April 30, 2022
:: Copyright (c) 2022-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies CARD_1, ORDINAL1, FUNCT_1, CLASSES1, TARSKI, ZFMISC_1, XBOOLE_0,
      RELAT_1, CARD_3, FUNCT_2, SUBSET_1, FINSET_1, ORDINAL2, CLASSES2,
      CLASSES4, PBOOLE, FACIRC_1, MCART_1, NAGATA_1, FUNCOP_1, CLASSES3,
      NUMBERS, ARYTM_2, ARYTM_3, MSAFREE, NAT_1, MATHMORP, YELLOW_6, QUATERNI,
      FINSEQ_1, FINSEQ_2, MATRIX_1, XXREAL_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, FINSET_1, RELAT_1,
      FUNCT_1, FUNCT_2, CLASSES1, CARD_3, ENS_1, PBOOLE, FUNCT_4, RELSET_1,
      ARYTM_2, ARYTM_3, MSAFREE, FUNCOP_1, XTUPLE_0, ORDINAL7, YELLOW_6,
      QUATERNI, EUCLID, FINSEQ_1, FINSEQ_2, MATRIX_0, CLASSES3, WELLORD2,
      DOMAIN_1, CLASSES2, XXREAL_0, ORDINAL1, NUMBERS, NAT_1, ORDINAL2,
      ORDERS_1;
 constructors CLASSES1, RELSET_1, CLASSES3, ARYTM_2, ENS_1, ORDINAL7, YELLOW_6,
      QUATERNI, EUCLID, MATRIX_0, CLASSES2, DOMAIN_1, BINARITH;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, CLASSES1, PBOOLE, FUNCT_4,
      RELSET_1, FUNCT_2, CLASSES2, CLASSES3, MSAFREE, ORDINAL5, FINSET_1,
      CARD_3, XTUPLE_0, FINSEQ_2, NUMBERS, SETFAM_1, XXREAL_0;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI;
 equalities TARSKI, ORDINAL1, CARD_3, NUMBERS, ARYTM_2, ARYTM_3, ENS_1,
      CLASSES2, QUATERNI, FUNCOP_1;
 expansions TARSKI, ORDINAL1, CLASSES1, XBOOLE_0, CLASSES3, FUNCT_2;
 theorems TARSKI, ZFMISC_1, ORDINAL1, ORDINAL2, FUNCT_1, FUNCT_2, CARD_1,
      CLASSES1, CARD_3, RELAT_1, XBOOLE_1, XBOOLE_0, FUNCT_4, PARTFUN1,
      CLASSES3, CLASSES2, XTUPLE_0, ORDINAL7, ORDINAL6, YELLOW_6, FINSEQ_1,
      FINSEQ_2, EUCLID, FUNCT_7, MSSUBLAT, ENUMSET1, FUNCT_5, NAT_1, XXREAL_0,
      ORDERS_1;
 schemes FUNCT_1, NAT_1, CLASSES1;

begin :: Preliminaries

theorem Th1:
  for X being set holds proj1 X in bool union union X &
  proj2 X in bool union union X
  proof
    let X be set;
    now
      thus proj1 X c= union union X
      proof
        let x be object;
        assume x in proj1 X;
        then ex y be object st [x,y] in X by XTUPLE_0:def 12;
        hence x in union union X by XTUPLE_0:6;
      end;
      thus proj2 X c= union union X
      proof
        let x be object;
        assume x in proj2 X;
        then ex y be object st [y,x] in X by XTUPLE_0:def 13;
        hence x in union union X by XTUPLE_0:7;
      end;
    end;
    hence thesis;
  end;

theorem
  REAL * = the set of all X where X is FinSequence of REAL
  proof
    now
      now
        let x be object;
        assume x in REAL *;
        then x is FinSequence of REAL by FINSEQ_1:def 11;
        hence x in the set of all X where X is FinSequence of REAL;
      end;
      hence REAL * c= the set of all X where X is FinSequence of REAL;
      now
        let x be object;
        assume x in the set of all X where X is FinSequence of REAL;
        then ex X be FinSequence of REAL st x = X;
        hence x in REAL * by FINSEQ_1:def 11;
      end;
      hence the set of all X where X is FinSequence of REAL c= REAL *;
    end;
    hence thesis;
  end;

registration
  cluster empty for Grothendieck;
  existence
  proof
    {} is power-closed & {} is FamUnion-closed;
    hence thesis;
  end;
end;

registration
  cluster non empty for Grothendieck;
  existence
  proof
    set G = the Grothendieck of {};
    {} in G by CLASSES3:def 4;
    hence thesis;
  end;
end;

registration
  let X be set;
  cluster -> non empty for Grothendieck of X;
  coherence by CLASSES3:def 4;
end;

begin :: Original definitions of Grothendieck's universe

definition
  let GU be set;
  attr GU is axiom_GU1 means
  for x,y being set st x in GU & y in x holds y in GU;

  attr GU is axiom_GU2 means
  for x,y being set st x in GU & y in GU holds {x,y} in GU;

  attr GU is axiom_GU3 means
  for x being set st x in GU holds bool x in GU;
end;

definition
  let GU be non empty set;
  attr GU is axiom_GU4 means
  for I being Element of GU
  for x being GU-valued ManySortedSet of I holds union rng x in GU;
end;

begin :: Equivalences of definitions

theorem Th3:
  for X being set holds X is axiom_GU1 iff X is epsilon-transitive
  proof
    let X be set;
    hereby
      assume X is axiom_GU1;
      then for x be set st x in X holds x c= X;
      hence X is epsilon-transitive;
    end;
    assume
A1: X is epsilon-transitive;
    now
      let x,y be set;
      assume that
A2:   y in x and
A3:   x in X;
      x c= X by A3,A1;
      hence y in X by A2;
    end;
    hence thesis;
  end;

theorem Th4:
  for X being non empty set holds X is axiom_GU4 iff X is FamUnion-closed
  proof
    let X be non empty set;
    hereby
      assume
A1:   X is axiom_GU4;
      now
        let A be set;
        let f be Function;
        assume that
A2:     dom f = A and
A3:     rng f c= X and
A4:     A in X;
        reconsider f9 = f as Function of A,X by A2,A3,FUNCT_2:2;
        reconsider f9 as X-valued ManySortedSet of A;
        union rng f9 in X by A4,A1;
        hence union rng f in X;
      end;
      hence X is FamUnion-closed;
    end;
    assume
A5: X is FamUnion-closed;
    now
      let I be Element of X;
      let x be X-valued ManySortedSet of I;
      dom x = I by PARTFUN1:def 2;
      hence union rng x in X by A5;
    end;
    hence X is axiom_GU4;
  end;

theorem
  for X being FamUnion-closed set, f being Function st dom f in X & rng f c= X
  holds union rng f in X by CLASSES3:def 3;

registration
  cluster -> axiom_GU1 axiom_GU2 axiom_GU3 for Grothendieck;
  coherence by Th3,CLASSES2:2,CLASSES3:def 1;
end;

registration
  cluster -> axiom_GU4 for non empty Grothendieck;
  coherence by Th4;
end;

theorem
  for G being non empty set st G is axiom_GU1 & G is axiom_GU2 &
  G is axiom_GU3 & G is axiom_GU4 holds G is non empty Grothendieck
    by Th3,Th4,CLASSES3:def 1;

theorem
  for X being set holds X is Universe iff X is non empty Grothendieck;

theorem Th8:
  for X being set holds
  Tarski-Class the_transitive-closure_of {X} is Grothendieck of X
  proof
    let X be set;
    set R = the_transitive-closure_of {X};
    set T = Tarski-Class R;
A1: union T c= T by CLASSES1:48;
    X in {X} & {X} c= R by CLASSES1:52,TARSKI:def 1;
    then X in R & R in T by CLASSES1:2;
    then X in union T by TARSKI:def 4;
    hence thesis by A1,CLASSES3:def 4;
  end;

theorem
  for X being set holds the_universe_of {X} is Grothendieck of X
  proof
    let X be set;
    the_universe_of {X} = Tarski-Class the_transitive-closure_of {X}
      by YELLOW_6:def 1;
    hence thesis by Th8;
  end;

theorem
  for X being set holds Universe_closure {X} = GrothendieckUniverse X
  proof
    let X be set;
    set UC = Universe_closure {X},
        GU = GrothendieckUniverse X;
    reconsider UC as Grothendieck;
A1: {X} c= Universe_closure {X} &
    for Y be Universe st {X} c= Y holds Universe_closure {X} c= Y
      by CLASSES2:def 4;
A2: for X,Y be set holds {X} c= Y iff X in Y
    proof
      let X,Y be set;
      hereby
        assume
A3:     {X} c= Y;
        X in {X} by TARSKI:def 1;
        hence X in Y by A3;
      end;
      assume X in Y;
      hence thesis by TARSKI:def 1;
    end;
    then reconsider UC as Grothendieck of X by A1,CLASSES3:def 4;
    for Y be Universe st X in Y holds Universe_closure {X} c= Y by A1,A2;
    then Universe_closure {X} c= GrothendieckUniverse X & GU c= UC
      by CLASSES3:def 4,def 5;
    hence thesis;
  end;

begin :: Equivalences of MacLane definition

theorem
  for U being Grothendieck st omega in U holds
  (for x,u being set st x in u in U holds x in U) &
  (for u,v being set st u in U & v in U holds {u,v} in U & [u,v] in U &
                                              [:u,v:] in U) &
  (for x being set st x in U holds bool x in U & union x in U) &
  (omega in U) &
  (for a,b being set for f being Function of a,b st dom f = a &
  f is onto & a in U & b c= U holds b in U)
  proof
    let U be Grothendieck;
    assume
A1: omega in U;
    then reconsider G = U as non empty Universe;
    hereby
      let x,u be set;
      assume
A2:   x in u in U;
      U is axiom_GU1;
      hence x in U by A2;
    end;
    hereby
      let u,v be set;
      assume that
A3:   u in U and
A4:   v in U;
      reconsider u9 = u,v9 = v as Element of G by A3,A4;
      {u9,v9} is Element of G & [u9,v9] is Element of G &
        [:u9,v9:] is Element of G;
      hence {u,v} in U & [u,v] in U & [:u,v:] in U;
    end;
    hereby
      let x be set;
      assume x in U;
      then reconsider x9 = x as Element of G;
      bool x9 in G & union x9 in G;
      hence bool x in U & union x in U;
    end;
    thus omega in U by A1;
    thus for a,b be set for f be Function of a,b st dom f = a &
      f is onto & a in U & b c= U holds b in U by CLASSES3:2;
  end;

theorem
  for U being set st
  (for x,u being set st x in u in U holds x in U) &
  (for x being set st x in U holds bool x in U & union x in U) &
  (omega in U) &
  (for a,b being set for f being Function of a,b st
  dom f = a & f is onto & a in U & b c= U holds b in U)
  holds U is Grothendieck
  proof
    let U be set;
    assume that
A1: for x,u being set st x in u in U holds x in U and
A2: for x being set st x in U holds bool x in U & union x in U and
A3: omega in U and
A4: for a,b being set for f being Function of a,b st
    dom f = a & f is onto & a in U & b c= U holds b in U;
    reconsider U9 = U as non empty set by A3;
    now
      thus U is axiom_GU1 by A1;
      thus U is axiom_GU3 by A2;
      now
        let Y be set;
        let f be Function;
        assume that
A5:     dom f = Y and
A6:     rng f c= U9 and
A7:     Y in U9;
        reconsider f9 = f as Function of Y,rng f by A5,FUNCT_2:1;
        f9 is onto;
        then rng f9 in U9 by A5,A6,A7,A4;
        hence union rng f in U9 by A2;
      end;
      then U9 is FamUnion-closed;
      hence U9 is axiom_GU4 by Th4;
    end;
    hence U is Grothendieck by Th3,Th4,CLASSES3:def 1;
  end;

begin :: Properties of Univers, following CLASSES2

reserve X for set;
reserve UN for Universe;

theorem Th13:
  X is axiom_GU1 & X is axiom_GU3
  implies
  (for y being set,
       x being Subset of y st y in X holds x in X) &
  (for x,y being set st x c= y & y in X holds x in X)&
  (X is non empty implies {} in X)
  proof
    assume that
A1: for x,y being set st x in X & y in x holds y in X and
A2: for x being set st x in X holds bool x in X;
A3: now
      let y be set;
      let x be Subset of y;
      assume y in X;
      then bool y in X by A2;
      hence x in X by A1;
    end;
    now
      assume X is non empty;
      then consider x be object such that
A4:   x in X;
      reconsider x9 = x as set by TARSKI:1;
      {} c= x9;
      hence {} in X by A4,A3;
    end;
    hence thesis by A3;
  end;

definition
  let UN be Universe;
  func {}UN -> Element of UN equals {};
  coherence by Th13;
end;

theorem
  UN is Grothendieck of {}
  proof
    {} in UN by Th13;
    hence thesis by CLASSES3:def 4;
  end;

theorem
  for u,v being Element of UN holds
  Funcs(u,v) c= the set of all f where f is Function of u,v
  proof
    let u,v be Element of UN;
    set F = the set of all f where f is Function of u,v;
    now
      let o be object;
      assume o in Funcs(u,v);
      then consider f be Function such that
A1:   o = f and
A2:   dom f = u and
A3:   rng f c= v by FUNCT_2:def 2;
      reconsider f as Function of u,v by A2,A3,FUNCT_2:2;
      f in F;
      hence o in F by A1;
    end;
    hence thesis;
  end;

definition
  let UN be Universe;
  let u be Element of UN;
  redefine func succ u -> Element of UN;  :: redefines succ (ORDINAL1, definition)
  coherence
  proof
    succ u = u \/ {u};
    hence thesis;
  end;
end;

theorem Th16:
  for n being Nat holds n in UN
  proof
    defpred P[Nat] means $1 in UN;
A1: P[0] by Th13;
    now
      let n be Nat;
      assume
A2:   P[n];
A3:   n (+) 1 = succ n by ORDINAL7:77;
      reconsider n9 = n as Element of UN by A2;
      succ n9 in UN;
      hence n + 1 in UN by A3,ORDINAL7:76;
    end;
    then
A4: for n be Nat st P[n] holds P[n + 1];
    for n be Nat holds P[n] from NAT_1:sch 2(A1,A4);
    hence thesis;
  end;

theorem
  omega c= UN by Th16;

theorem
  NAT in UN or NAT,UN are_equipotent
  proof
    NAT c= UN by Th16;
    hence thesis by CLASSES1:def 2;
  end;

registration
  cluster -> infinite for Universe;
  coherence
  proof
    let UN be Universe;
A1: omega c= UN by Th16;
    assume UN is finite;
    hence thesis by A1;
  end;
end;

theorem Th19:
  FinSETS is denumerable by CLASSES2:62,64,CARD_3:def 15;

registration
  cluster denumerable for Universe;
  existence by Th19;
end;

theorem Th20:
  not UN is denumerable iff omega in UN
  proof
    hereby
      assume not UN is denumerable;
      then UN is uncountable;
      hence omega in UN by ORDINAL6:57;
    end;
    assume omega in UN;
    hence not UN is denumerable by ORDINAL6:57;
  end;

registration
  cluster non denumerable for Universe;
  existence
  proof
    set GX = the Grothendieck of NAT;
    NAT in GX by CLASSES3:def 4;
    hence thesis by Th20;
  end;
end;

definition
  let UN be Universe;
  attr UN is trivial means
:Def6:
  not omega in UN;
end;

theorem Th21:
  FinSETS is trivial & SETS is non trivial
  proof
    SETS is_Tarski-Class_of FinSETS by CLASSES1:def 4;
    then omega c= FinSETS in SETS & SETS is axiom_GU1 & SETS is axiom_GU3
      by Th16;
    hence thesis by Th13,Th19,Th20;
end;

registration
  cluster trivial for Universe;
  existence
  proof
    set UN = FinSETS;
    take UN;
    thus thesis by Th19,Th20;
  end;
end;

registration
  cluster non trivial for Universe;
  existence by Th21;
end;

registration
  cluster -> non denumerable for non trivial Universe;
  coherence by Def6,Th20;
end;

theorem
  for x being Element of UN for y,z being object st x = [y,z] holds
  y is Element of UN & z is Element of UN
  proof
    let x be Element of UN;
    let y,z be object;
    assume
A1: x = [y,z];
A2: UN is axiom_GU1;
    {y} in x in UN by A1,TARSKI:def 2;
    then y in {y} in UN by A2,TARSKI:def 1;
    hence y is Element of UN by A2;
    {y,z} in x in UN by A1,TARSKI:def 2;
    then z in {y,z} in UN by A2,TARSKI:def 2;
    hence z is Element of UN by A2;
  end;

registration
  let UN being Universe;
  cluster pair for Element of UN;
  existence
  proof
    set u = the Element of UN;
    take [ u,u ];
    thus thesis;
  end;
end;

theorem
  for u,v being Element of UN holds
  the set of all f where f is Function of u,v is Element of UN
  proof
    let u,v be Element of UN;
    set S = the set of all f where f is Function of u,v;
    S is Subset of bool [: u, v :]
    proof
      now
        let o be object;
        assume o in S;
        then ex f be Function of u,v st o = f;
        hence o in bool [:u,v:];
      end;
      then S c= bool [:u,v:];
      hence thesis;
    end;
    hence thesis by Th13;
  end;

definition
  let UN being Universe,
      I being Element of UN,
      x being UN-valued ManySortedSet of I;
  redefine func product x -> Element of UN;  :: redefines product (CARD_3, definition)
  coherence
  proof
    dom x = I & rng x c= UN by PARTFUN1:def 2;
    hence thesis by YELLOW_6:1;
  end;
end;

Lm1:
  for x,y,a,b being set holds (x,y) --> (a,b) c= [:{x,y},{a,b}:]
  proof
    let x,y,a,b be set;
    set f = (x,y) --> (a,b);
    now
      thus f c= [:dom f,rng f:] by RELAT_1:7;
      dom f = {x,y} & rng f c= {a,b} by FUNCT_4:62;
      hence [:dom f,rng f:] c= [:{x,y},{a,b}:] by ZFMISC_1:96;
    end;
    hence thesis;
  end;

definition
  let UN being Universe;
  let x,y being Element of UN;
  func disjoint-union(x,y) -> Element of UN
  equals
    (x,y) --> ({}UN, {{}UN});
  coherence
  proof
    reconsider f = (x,y) --> ({}UN, {{}UN}) as Function;
    f c= [:{x,y},{ {}UN,{{}UN}}:] by Lm1;
    hence thesis by Th13;
  end;
end;

theorem
  for x,y being Element of UN holds
  disjoint-union(x,y) is Subset of [:{x,y},{ {}, {{}} }:] by Lm1;

theorem
  for u being Element of UN holds
  disjoint-union(u,u) = { [ u , {{}} ] }
  proof
    let u be Element of UN;
    disjoint-union(u,u) = u .--> {{}UN} by FUNCT_4:81
                       .= { [u,{{}UN}] } by FUNCT_4:82;
    hence thesis;
  end;

definition
  let UN be Universe;
  let I be Element of UN;
  let x be UN-valued ManySortedSet of I;
  redefine func dom x -> Element of UN;  :: redefines dom (RELAT_1, synonym) → proj1 (XTUPLE_0, definition)
  coherence by PARTFUN1:def 2;
end;

definition
  let UN be Universe;
  let I be Element of UN;
  let x be UN-valued ManySortedSet of I;
  redefine func Union x -> Element of UN;  :: redefines Union (CARD_3, definition)
  coherence
  proof
    set G = UN;
    G is axiom_GU4 & Union x = union rng x;
    hence thesis;
  end;
end;

definition
  let UN be Universe;
  let I be Element of UN;
  let x be UN-valued ManySortedSet of I;
  redefine func disjoin x -> UN-valued ManySortedSet of I;  :: redefines disjoin (CARD_3, definition)
  coherence
  proof
    set G = UN;
A1: dom disjoin x = I by PARTFUN1:def 2;
A2: dom x = I by PARTFUN1:def 2;
    reconsider domx = dom x as Element of G;
    reconsider dx = disjoin x as I-defined Function;
A3: rng disjoin x c= G
    proof
      let o be object;
      assume o in rng disjoin x;
      then consider o9 be object such that
A4:   o9 in dom dx and
A5:   o = dx.o9 by FUNCT_1:def 3;
A6:   G is axiom_GU1;
A7:   o9 in dom x by A4,CARD_3:def 3;
      reconsider o9 as Element of G by A6,A4;
A8:   o = [: x.o9,{o9} :] by A7,A5,CARD_3:def 3;
      now
        x.o9 in rng x by A4,A2,FUNCT_1:def 3;
        hence x.o9 in G;
        thus {o9} in G;
      end;
      then reconsider xo9 = x.o9, enso9 = {o9} as Element of G;
      [: xo9, enso9 :] is Element of G;
      hence thesis by A8;
    end;
    reconsider dx = disjoin x as Function of I,G by A1,A3,FUNCT_2:2;
    dx is G-valued ManySortedSet of I;
    hence thesis;
  end;
end;

definition
  let UN be Universe;
  let I be Element of UN;
  let x be UN-valued ManySortedSet of I;
  func disjoint-union x -> Element of UN equals Union disjoin x;
  coherence;
end;

theorem
  for I being Element of UN
  for x being UN-valued ManySortedSet of I holds
  Union coprod x is Element of UN
  proof
    let I be Element of UN;
    let x be UN-valued ManySortedSet of I;
    Union disjoin x is Element of UN;
    hence thesis;
  end;

theorem
  for I being Element of UN,
      x being UN-valued ManySortedSet of I
  holds disjoint-union x is Subset of [: union rng x,I :]
  proof
    let I be Element of UN;
    let x be UN-valued ManySortedSet of I;
    union rng disjoin x c= [: union rng x,I :]
    proof
      let o be object;
      assume o in union rng disjoin x;
      then consider o9 be set such that
A1:   o in o9 and
A2:   o9 in rng disjoin x by TARSKI:def 4;
      consider y be object such that
A3:   y in dom disjoin x and
A4:   o9 = (disjoin x).y by A2,FUNCT_1:def 3;
A5:   y in dom x by A3,CARD_3:def 3;
A6:   y in I by A3,PARTFUN1:def 2;
A7:   o in [: x.y,{y} :] by A1,A4,A5,CARD_3:def 3;
      now
        let o be object;
        assume o in [: x.y,{y} :];
        then consider o1,o2 be object such that
A8:     o1 in x.y and
A9:     o2 in {y} and
A10:     o = [o1,o2] by ZFMISC_1:def 2;
        now
          x.y in rng x by A5,FUNCT_1:def 3;
          hence o1 in union rng x by A8,TARSKI:def 4;
          thus o2 in I by A6,A9,TARSKI:def 1;
        end;
        hence o in [: union rng x,I:] by A10,ZFMISC_1:def 2;
      end;
      hence thesis by A7;
    end;
    hence thesis;
  end;

theorem
  X is axiom_GU2
  implies
  (for x being set st x in X holds {x} in X)
  proof
    assume
A1: X is axiom_GU2;
    let x be set;
    assume
A2: x in X;
    {x} = {x,x} by ENUMSET1:29;
    hence {x} in X by A1,A2;
  end;

theorem
  for u being Element of UN holds card u in UN by CLASSES2:11;

theorem
  for u being Element of UN holds
  not u,UN are_equipotent & card u in card UN by CLASSES2:1;

theorem Th31:
  for u,v being Element of UN holds
  { [u, {} ], [v, {{}} ] } = [: {u}, { {} } :] \/ [: {v}, { {{}} }:]
  proof
    let u,v be Element of UN;
    set S1 = { [u, {} ] , [v, {{}} ] },
        S2 = [: {u}, { {} } :] \/ [: {v}, { {{}} }:];
    now
      now
        let o be object;
        assume o in S1;
        then o = [u,{}] or o = [v,{{}}] by TARSKI:def 2;
        then o in [:{u},{{}}:] or o in [:{v},{ {{}} }:] by ZFMISC_1:28;
        hence o in S2 by XBOOLE_0:def 3;
      end;
      hence S1 c= S2;
      now
        let o be object;
        assume o in S2;
        then o in [: {u}, { {} } :] or o in [: {v}, { {{}} }:]
          by XBOOLE_0:def 3;
        then o in {[u,{}]} or o in {[v,{{}}]} by ZFMISC_1:29;
        then o = [u,{}] or o = [v,{{}}] by TARSKI:def 1;
        hence o in S1 by TARSKI:def 2;
      end;
      hence S2 c= S1;
    end;
    hence thesis;
  end;

theorem Th32:
  for I,a,b,u,v being Element of UN
  for x being UN-valued ManySortedSet of I st
  I = { a, b } & x.a = u & x.b = v holds
  disjoint-union x = [: u, { a } :] \/ [: v, { b }:]
  proof
    let I,a,b,u,v be Element of UN;
    let x be UN-valued ManySortedSet of I;
    assume that
A1: I = { a, b } and
A2: x.a = u and
A3: x.b = v;
A4: dom disjoin x = dom x & for o be object st o in dom x holds
      (disjoin x).o = [: x.o , {o} :] by CARD_3:def 3;
A5: dom x = { a, b } by A1,PARTFUN1:def 2;
    then a in dom x & b in dom x by TARSKI:def 2;
    then
A6: (disjoin x).a = [: x.a, { a } :] & (disjoin x).b = [: x.b, { b }:]
      by CARD_3:def 3;
    set S = { [: x.a, { a } :], [: x.b, { b }:] };
    rng disjoin x = { [: x.a, { a } :], [: x.b, { b }:] }
    proof
      now
        now
          let o be object;
          assume o in rng disjoin x;
          then consider o9 be object such that
A7:       o9 in dom disjoin x and
A8:       o = (disjoin x).o9 by FUNCT_1:def 3;
          o9 = a or o9 = b by A7,A4,A5,TARSKI:def 2;
          hence o in S by A8,A6,TARSKI:def 2;
        end;
        hence rng disjoin x c= S;
        now
          let o be object;
          assume o in S; then
A9:       o = (disjoin x).a or o = (disjoin x).b by A6,TARSKI:def 2;
          a in dom disjoin x & b in dom disjoin x by A4,A5,TARSKI:def 2;
          hence o in rng disjoin x by A9,FUNCT_1:def 3;
        end;
        hence S c= rng disjoin x;
      end;
      hence thesis;
    end;
    hence thesis by A2,A3,ZFMISC_1:75;
  end;

theorem Th33:
  for I,u,v being Element of UN
  for x being UN-valued ManySortedSet of I st
  I = { {}, {{}} } & x.{} = u & x.{{}} = v holds
  disjoint-union x = [: u, { {} } :] \/ [: v, { {{}} }:]
  proof
    let I,u,v be Element of UN;
    let x be UN-valued ManySortedSet of I;
    assume
A1: I = { {}, {{}} } & x.{} = u & x.{{}} = v;
    {}UN is Element of UN & {{}UN} is Element of UN;
    hence thesis by A1,Th32;
  end;

theorem
  for I,u,v being Element of UN
  for x being UN-valued ManySortedSet of I st
  I = { {}, {{}} } & x.{} = {u} & x.{{}} = {v} & u <> v holds
    disjoint-union x = disjoint-union (u,v)
  proof
    let I,u,v be Element of UN;
    let x be UN-valued ManySortedSet of I;
    assume that
A1: I = { {}, {{}} } and
A2: x.{} = {u} and
A3: x.{{}} = {v} and
A4: u <> v;
    disjoint-union(u,v) = { [u, {} ] , [v, {{}} ] } &
      disjoint-union x = [: {u}, { {} } :] \/ [: {v}, { {{}} }:]
      by A1,A2,A3,Th33,A4,FUNCT_4:67;
    hence thesis by Th31;
  end;

theorem Th35:
  for x being Element of UN
  for y,z being object st x = [y,z] holds y is Element of UN &
  z is Element of UN
  proof
    let x be Element of UN;
    let y,z be object;
    assume
A1: x = [y,z];
A2: UN is axiom_GU1;
    {y} in x in UN by A1,TARSKI:def 2;
    then y in {y} in UN by A2,TARSKI:def 1;
    hence y is Element of UN by A2;
    {y,z} in x in UN by A1,TARSKI:def 2;
    then z in {y,z} in UN by A2,TARSKI:def 2;
    hence z is Element of UN by A2;
  end;

registration
  let UN being Universe;
  cluster pair for Element of UN;
  existence
  proof
    set u = the Element of UN;
    take [ u,u ];
    thus thesis;
  end;
end;

definition
  let UN be Universe;
  let u be pair Element of UN;
  redefine func u`1 -> Element of UN;  :: redefines `1 (XTUPLE_0, definition)
  coherence
  proof
    ex u1,u2 be object st u = [u1,u2] by XTUPLE_0:def 1;
    hence thesis by Th35;
  end;
  redefine func u`2 -> Element of UN;  :: redefines `2 (XTUPLE_0, definition)
  coherence
  proof
    ex u1,u2 be object st u = [u1,u2] by XTUPLE_0:def 1;
    hence thesis by Th35;
  end;
end;

theorem Th36:
  for X being Element of UN holds proj1 X is Element of UN &
  proj2 X is Element of UN
  proof
    let X be Element of UN;
    proj1 X in bool union union X &
      proj2 X in bool union union X &
      UN is axiom_GU1 by Th1;
    hence thesis;
  end;

theorem Th37:
  for R being Relation st R in UN holds dom R in UN & rng R in UN
  proof
    let R be Relation;
    assume R in UN;
    then dom R is Element of UN & rng R is Element of UN by Th36;
    hence thesis;
  end;

theorem
  for R being Relation st dom R is Element of UN &
  rng R is Element of UN holds R is Element of UN
  proof
    let R be Relation;
    assume that
A1: dom R is Element of UN and
A2: rng R is Element of UN;
A3: R c= [: dom R, rng R :] by RELAT_1:7;
    [: dom R, rng R:] is Element of UN by A1,A2,CLASSES2:61;
    hence thesis by A3,Th13;
  end;

theorem
  for X being set,Y being non empty set, f being Function of X,Y st
  f in UN holds X in UN
  proof
    let X be set;
    let Y be non empty set;
    let f be Function of X,Y;
    assume
A1: f in UN;
    dom f = X by FUNCT_2:def 1;
    hence thesis by A1,Th37;
  end;

theorem
  for A,B being non empty set st [:A,B:] is Element of UN holds
  A is Element of UN & B is Element of UN
  proof
    let A,B be non empty set;
    assume
A1: [:A,B:] is Element of UN;
    proj1 [:A,B:] = A & proj2 [:A,B:] = B by FUNCT_5:9;
    hence thesis by A1,Th36;
 end;

theorem
  for X being set st id X is Element of UN holds X is Element of UN
  proof
    let X be set;
    assume id X is Element of UN;
    then dom id X in UN by Th37;
    hence thesis by RELAT_1:45;
  end;

theorem
  for x,y,z being Element of UN holds (x,y) .--> z is Element of UN
  proof
    let x,y,z be Element of UN;
    (x,y) .--> z = [: {[x,y]} , {z} :];
    hence thesis;
  end;

begin

theorem Th43:
  omega c< FinSETS
  proof
A1: omega c= FinSETS by Th16;
    now
      assume
A2:   omega = FinSETS;
      then reconsider x1 = 1 as Element of FinSETS;
      {x1} in FinSETS;
      then
A3:   {1} is epsilon-transitive by A2;
      not 1 c= {1}
      proof
        assume
A5:     1 c= {1};
        0 in 1 by CARD_1:49,TARSKI:def 1;
        hence thesis by A5;
      end;
      hence thesis by A3;
    end;
    hence thesis by A1;
  end;

theorem Th44:
  for X being set holds Tarski-Class {} c= Tarski-Class X
  proof
    let X be set;
    set T1 = Tarski-Class {},
        T2 = Tarski-Class X;
A1: T1 is_Tarski-Class_of {} & for D be set st D is_Tarski-Class_of {}
    holds T1 c= D by CLASSES1:def 4;
    {} c= T2 & T2 is Tarski & not T2,{} are_equipotent by CARD_1:26;
    then {} in T2;
    hence thesis by A1,CLASSES1:def 3;
  end;

theorem Th45:
  for G being Grothendieck of X holds FinSETS c= G
  proof
    let G be Grothendieck of X;
    FinSETS c= Tarski-Class X & Tarski-Class X c= G by Th44,CLASSES3:18;
    hence thesis;
  end;

theorem Th46:
  GrothendieckUniverse {} = FinSETS & GrothendieckUniverse {} = UNIVERSE {}
    by Th45,CLASSES2:65,56,CLASSES3:21;

theorem
  for X being set
  for G being Grothendieck of X
  holds GrothendieckUniverse {} c= GrothendieckUniverse X c= G
    by CLASSES2:56,CLASSES3:21,CLASSES3:def 5;

theorem
  for n being Element of FinSETS holds GrothendieckUniverse n = FinSETS
  proof
    let n be Element of FinSETS;
    FinSETS is Grothendieck of n by CLASSES3:def 4;
    hence thesis by Th45,CLASSES3:def 5;
  end;

theorem
  the empty Grothendieck c< omega c< GrothendieckUniverse {} c<
    GrothendieckUniverse omega
  proof
    set GU0     = GrothendieckUniverse {},
        GUomega = GrothendieckUniverse omega;
    the empty Grothendieck c= omega c= GU0 c= GUomega by Th16,CLASSES3:21;
    hence thesis by Th46,Th43,Th19,Th20,CLASSES3:def 4;
  end;

theorem
  for G being non empty Grothendieck st
  G <> GrothendieckUniverse omega holds
  GrothendieckUniverse omega in G or G in GrothendieckUniverse omega
  by CLASSES2:52;

theorem
  Tarski-Class omega = GrothendieckUniverse omega by CLASSES3:22;

theorem Th52:
  for N1,N2 being set st N1 = [:NAT,NAT:] \/ NAT &
                         N2 = N1 \/ bool N1 holds
  REAL c= N2 \/ [:NAT,N2:]
  proof
    set F1 = {[i,j] where i,j is Element of omega: i,j are_coprime & j <> {}},
        F2 = the set of all [k,1] where k is Element of omega;
    F1 c= [:NAT,NAT:]
    proof
      let o be object;
      assume o in F1;
      then ex i,j be Element of omega st o = [i,j] & i,j are_coprime & j <> {};
      hence thesis;
    end;
    then F1 \ F2 c= [:NAT,NAT:];
    then
A1: RAT+ c= [:NAT,NAT:] \/ NAT by XBOOLE_1:13;
    then
A2: RAT+ \/ DEDEKIND_CUTS c= ([:NAT,NAT:] \/ NAT) \/ DEDEKIND_CUTS
      by XBOOLE_1:9;
A3: bool RAT+ c= bool ([:NAT,NAT:] \/ NAT) by A1,ZFMISC_1:67;
A4: REAL+ c= ([:NAT,NAT:] \/ NAT) \/ DEDEKIND_CUTS by A2;
A5: ([:NAT,NAT:] \/ NAT) \/ DEDEKIND_CUTS
      c= ([:NAT,NAT:] \/ NAT) \/ bool RAT+ by XBOOLE_1:9;
    ([:NAT,NAT:] \/ NAT) \/ bool RAT+
      c= ([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT) \/
      bool ([:NAT,NAT:] \/ NAT) by A3,XBOOLE_1:9;
    then
A6: REAL+ c= ([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT)
      \/ bool ([:NAT,NAT:] \/ NAT) by A4,A5;
    then [:NAT,REAL+:] c= [:NAT, ([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT)
      \/ bool ([:NAT,NAT:] \/ NAT):] by ZFMISC_1:96; then
A7: REAL+ \/ [:NAT,REAL+:] c=
      (([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT) \/
        bool ([:NAT,NAT:] \/ NAT))
        \/ [:NAT, ([:NAT,NAT:] \/ NAT) \/ ([:NAT,NAT:] \/ NAT) \/
        bool ([:NAT,NAT:] \/ NAT):] by A6,XBOOLE_1:13;
    set N1 = [:NAT,NAT:] \/ NAT,
        N2 = N1 \/ bool N1;
    [:{0},REAL+:] c= [:NAT,REAL+:] by ZFMISC_1:96;
    then REAL+ \/ [:{0},REAL+:] c= REAL+ \/ [:NAT,REAL+:] by XBOOLE_1:9;
    hence thesis by A7;
  end;

theorem Th53:
  for UN being non trivial Universe holds REAL is Element of UN
  proof
    let UN be non trivial Universe;
    reconsider n = NAT as Element of UN by Def6;
    reconsider n1 = [:n,n:] \/ n as Element of UN;
    reconsider n2 = n1 \/ bool n1 as Element of UN;
    REAL c= n2 \/ [:n,n2:] by Th52;
    hence thesis by Th13;
  end;

theorem Th54:
  for UN being non trivial Universe holds ExtREAL is Element of UN
  proof
    let UN being non trivial Universe;
    reconsider u = REAL as Element of UN by Th53;
    0 is Element of UN by Th13;
    then [0,u] is Element of UN by CLASSES2:3;
    then {u,[0,u]} is Element of UN by CLASSES2:2;
    hence thesis by CLASSES2:60;
  end;

theorem Th55:
  for UN being non trivial Universe holds COMPLEX in UN
  proof
    let UN be non trivial Universe;
    set X = Funcs({0,1},REAL),
        Y = {x where x is Element of Funcs({0,1},REAL): x.1 = 0};
A1: (X \ Y) \/ REAL c= X \/ REAL by XBOOLE_1:13;
A2: 0 in UN & 1 in UN by Th16;
    UN is axiom_GU2;
    then
A3: {0,1} in UN by A2;
A4: REAL is Element of UN by Th53;
    then Funcs({0,1},REAL) in UN by A3,CLASSES2:61;
    then X \/ REAL in UN by A4,CLASSES2:60;
    hence thesis by Th13,A1;
  end;

theorem Th56:
  for UN being non trivial Universe holds QUATERNION in UN
  proof
    let UN be non trivial Universe;
A1: QUATERNION c= Funcs(4,REAL) \/ COMPLEX by XBOOLE_1:13;
    4 in UN & REAL is Element of UN by Th16,Th53;
    then Funcs(4,REAL) in UN & COMPLEX in UN by Th55,CLASSES2:61;
    then Funcs(4,REAL) \/ COMPLEX in UN by CLASSES2:60;
    hence thesis by A1,Th13;
  end;

theorem Th57:
  for n being Nat holds Seg n in UN
  proof
    let n be Nat;
    n + 1 in UN & Seg n = (n + 1) \ {0} by FINSEQ_1:83,Th16;
    hence thesis by Th13;
  end;

theorem Th58:
  for D being set st D in UN holds for n being Nat holds n-tuples_on D in UN
  proof
    let D be set;
    assume
A1: D in UN;
    let n be Nat;
    Seg n in UN by Th57;
    then Funcs(Seg n,D) in UN by A1,CLASSES2:61;
    hence thesis by FINSEQ_2:93;
  end;

theorem
  for UN being non trivial Universe, n being Nat holds REAL n in UN
  proof
    let UN be non trivial Universe;
    let n be Nat;
    REAL is Element of UN & n-tuples_on REAL = REAL n by EUCLID:def 1,Th53;
    hence thesis by Th58;
  end;

theorem
  for X being set st X in UN holds for n being Nat holds n-tuples_on X in UN
  proof
    let X be set;
    assume
A1: X in UN;
    let n be Nat;
    Seg n in UN by Th57;
    then Funcs(Seg n,X) in UN by A1,CLASSES2:61;
    hence thesis by FINSEQ_2:93;
  end;

theorem
  for X being set for n being Nat holds n-tuples_on X c= X* by FINSEQ_2:90;

theorem Th62:
  for X being non empty set for x being object st x in X* holds
  ex n being Nat st x in n-tuples_on X
  proof
    let X be non empty set;
    let x be object;
    assume x in X*;
    then reconsider x as Element of X*;
    reconsider y = x as FinSequence of X;
    take len y;
    y is Element of (len y)-tuples_on X by FINSEQ_2:92;
    hence thesis;
  end;

theorem Th63:
  for X being non empty set ex f being Function st dom f = NAT &
  (for n being Nat holds f.n = n-tuples_on X) & union rng f = X*
  proof
    let X be non empty set;
    defpred P[object,object] means ex n be Nat st $1 = n & $2 = n-tuples_on X;
A1: for x,y1,y2 be object st x in NAT & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x be object st x in NAT ex y be object st P[x,y]
    proof
      let x be object;
      assume x in NAT;
      then reconsider z = x as Nat;
      take z-tuples_on X;
      thus thesis;
    end;
    consider f be Function such that
A3: dom f = NAT and
A4: for x be object st x in NAT holds P[x,f.x] from FUNCT_1:sch 2(A1,A2);
A5: for n be Nat holds f.n = n-tuples_on X
    proof
      let n be Nat;
      P[n,f.n] by A4,ORDINAL1:def 12;
      hence thesis;
    end;
    union rng f = X*
    proof
      now
        now
          let x be object;
          assume x in union rng f;
          then consider y be set such that
A6:       x in y and
A7:       y in rng f by TARSKI:def 4;
          consider z be object such that
A8:       z in dom f and
A9:       y = f.z by A7,FUNCT_1:def 3;
          reconsider z as Nat by A3,A8;
A10:      x in z-tuples_on X by A5,A6,A9;
          z-tuples_on X c= X * by FINSEQ_2:90;
          hence x in X * by A10;
        end;
        hence union rng f c= X *;
        now
          let x be object;
          assume x in X*;
          then consider n be Nat such that
A11:      x in n-tuples_on X by Th62;
          n-tuples_on X in rng f
          proof
A12:        n in dom f by A3,ORDINAL1:def 12;
            f.n = n-tuples_on X by A5;
            hence thesis by A12,FUNCT_1:def 3;
          end;
          hence x in union rng f by A11,TARSKI:def 4;
        end;
        hence X* c= union rng f;
      end;
      hence thesis;
    end;
    hence thesis by A3,A5;
  end;

theorem Th64:
  for UN being non trivial Universe, X being non empty set st X in UN
  holds X* in UN
  proof
    let UN be non trivial Universe;
    let X be non empty set;
    assume
A1: X in UN;
    consider f be Function such that
A2: dom f = NAT and
A3: for n be Nat holds f.n = n-tuples_on X and
A4: union rng f = X* by Th63;
    now
      thus UN is FamUnion-closed;
      thus dom f = omega by A2;
      now
        let x be object;
        assume x in rng f;
        then consider y be object such that
A5:     y in dom f and
A6:     x = f.y by FUNCT_1:def 3;
        reconsider y as Nat by A5,A2;
        y-tuples_on X in UN by A1,Th58;
        hence x in UN by A6,A3;
      end;
      hence rng f c= UN;
    end;
    hence thesis by Def6,A4;
  end;

theorem
  for UN being non trivial Universe holds REAL * in UN
  proof
    let UN be non trivial Universe;
    REAL is Element of UN by Th53;
    hence thesis by Th64;
  end;

theorem
  for UN being non trivial Universe holds ExtREAL * in UN
  proof
    let UN be non trivial Universe;
    ExtREAL is Element of UN by Th54;
    hence thesis by Th64;
  end;

theorem
  for UN being non trivial Universe holds COMPLEX * in UN by Th64,Th55;

theorem
  for UN being non trivial Universe holds QUATERNION * in UN by Th64,Th56;

theorem Th69:
  for UN being Universe
  for X being set st X in UN holds
  for s being FinSequence of X holds s in UN
  proof
    let UN be Universe;
    let X be set;
    assume
A1: X in UN;
    let s be FinSequence of X;
    consider n be Nat such that
A2: dom s = Seg n by FINSEQ_1:def 2;
    rng s c= X;
    then
A3: s is Function of dom s,X by FUNCT_2:2;
    Seg n in UN by Th57;
    then [: Seg n, X:] in UN by A1,CLASSES2:61;
    hence thesis by A3,A2,Th13;
  end;

theorem
  for X being empty set
  for f being FinSequence of X* holds f = (len f) |-> 0
  by FUNCT_7:17,MSSUBLAT:5;

theorem
  for UN being non trivial Universe, D being non empty set st D in UN holds
  for M being Matrix of D holds M in UN by Th64,Th69;

theorem Th72:
  FinSETS in SETS & NAT in SETS & REAL in SETS & ExtREAL in SETS
  proof
    SETS is_Tarski-Class_of FinSETS by CLASSES1:def 4;
    then
A1: omega c= FinSETS in SETS & SETS is axiom_GU1 & SETS is axiom_GU3 by Th16;
    then NAT in SETS & SETS is Grothendieck by Th13;
    then reconsider X = SETS as non trivial Universe by Def6;
    REAL is Element of X & ExtREAL is Element of X by Th53,Th54;
    hence thesis by A1,Th13;
  end;

theorem Th73:
  for X being set
  for U1 being Universe st U1 in Tarski-Class X
  holds Tarski-Class U1 c= Tarski-Class X
  proof
    let X be set;
    let U1 be Universe;
    assume U1 in Tarski-Class X;
    then Tarski-Class X is_Tarski-Class_of U1;
    hence thesis by CLASSES1:def 4;
  end;

theorem Th74:
  FinSETS in Tarski-Class omega
  proof
    not Tarski-Class omega c= FinSETS by Th19,Th20,CLASSES1:2;
    hence thesis by CLASSES2:53;
  end;

theorem Th75:
  SETS = Tarski-Class omega
  proof
    SETS is Grothendieck of omega by Th72,CLASSES3:def 4;
    hence thesis by Th73,Th74,CLASSES3:18;
  end;

theorem
  GrothendieckUniverse omega = SETS by CLASSES3:22,Th75;

theorem Th77:
  GrothendieckUniverse omega = GrothendieckUniverse FinSETS = SETS
  proof
    GrothendieckUniverse omega = GrothendieckUniverse FinSETS
    proof
      GrothendieckUniverse omega = SETS by CLASSES3:22,Th75;
      hence thesis by CLASSES3:22;
    end;
    hence thesis by CLASSES3:22;
  end;

theorem Th78:
  for X being non empty set
  for GX being Grothendieck of X
  for G being Universe st X misses G
  holds GX <> G
  proof
    let X be non empty set;
    let GX be Grothendieck of X;
    let G be Universe;
    assume
A1: X misses G;
    assume GX = G;
    then X in G & G is axiom_GU1 & G is axiom_GU3 by CLASSES3:def 4;
    then X c= G;
    hence thesis by A1,XBOOLE_1:68;
  end;

theorem
  for X being non empty set
  for GX being Grothendieck of X
  for G being Universe st X misses G
  holds GX in G or G in GX by Th78,CLASSES2:52;

theorem
  for UN1,UN2 being Universe
  for a being Element of UN1 st not a in UN2 holds UN2 in UN1
  proof
    let G1,G2 be Universe;
    let a be Element of G1;
    assume
A1: not a in G2;
A2: G1 is Grothendieck of {a} by CLASSES3:def 4;
A3: now
      assume {a} meets G2;
      then {a} /\ G2 is non empty;
      then consider z be object such that
A4:   z in {a} /\ G2;
      z in {a} & z in G2 by A4,XBOOLE_0:def 4;
      hence contradiction by A1,TARSKI:def 1;
    end;
    now
      assume
A5:   G1 in G2;
      G2 is axiom_GU1 & G2 is axiom_GU3;
      hence contradiction by A1,A5;
    end;
    hence thesis by A3,A2,Th78,CLASSES2:52;
  end;

theorem Th81:
  for G being Grothendieck holds union G = G
  proof
    let G be Grothendieck;
    per cases;
    suppose G is empty;
      hence thesis by ZFMISC_1:2;
    end;
    suppose G is non empty;
      then reconsider G as non empty Grothendieck;
      now
        now
          let o be object;
          assume o in union G;
          then consider o9 be set such that
A1:       o in o9 in G by TARSKI:def 4;
          reconsider o9 as Element of G by A1;
          G is axiom_GU1;
          hence o in G by A1;
        end;
        hence union G c= G;
        now
          let o be object;
          assume o in G;
          then reconsider o9 = o as Element of G;
          o in {o9} in G by TARSKI:def 1;
          hence o in union G by TARSKI:def 4;
        end;
        hence G c= union G;
      end;
      hence thesis;
    end;
  end;

registration
  cluster -> limit_ordinal for Grothendieck;
  coherence by Th81;
end;

theorem
  for UN being Universe, V being non empty Element of UN
  holds Funcs(V) is Subset of UN
  proof
    let UN be Universe;
    let V be non empty Element of UN;
    now
      let o be object;
      assume o in the set of all Funcs(A,B) where A,B is Element of V;
      then consider A,B be Element of V such that
A1:   o = Funcs(A,B);
A2:   UN is axiom_GU1;
      reconsider A,B as Element of UN by A2;
      Funcs(A,B) in UN;
      hence o in UN by A1;
    end;
    then the set of all Funcs(A,B) where A,B is Element of V c= UN;
    then union the set of all Funcs(A,B) where A,B is Element of V c= union UN
      by ZFMISC_1:77;
    hence thesis by Th81;
  end;

begin :: How to get out of a universe ?

theorem
  ex a being set st not a in UN
  proof
    assume for a be set holds a in UN;
    then UN in UN;
    hence contradiction;
  end;

theorem
  ex A being Subset of UN st not A in UN
  proof
    assume
A1: for A be Subset of UN holds A in UN;
    UN c= UN;
    then UN in UN by A1;
    hence contradiction;
  end;

theorem
  not the set of all u where u is Element of UN is Element of UN
  proof
    set SETUN = the set of all u where u is Element of UN;
    assume
A1: SETUN is Element of UN;
    now
      thus SETUN c= UN
      proof
        let o be object;
        assume o in SETUN;
        then ex u be Element of UN st o = u;
        hence o in UN;
      end;
      thus UN c= SETUN;
    end;
    then SETUN = UN;
    then UN in UN by A1;
    hence thesis;
  end;

theorem Th86:
  for X being Element of UN holds not UN \ X is Element of UN
  proof
    let X be Element of UN;
    not UN \ X in UN
    proof
      assume UN \ X in UN;
      then
A1:   (UN \ X) \/ X in UN by CLASSES2:60;
A2:   (UN \ X) \/ X = UN \/ X by XBOOLE_1:39;
A3:   UN \/ X c= UN
      proof
        let x be object;
        assume x in UN \/ X;
        then x in UN or (x in X in UN) & UN is axiom_GU1 by XBOOLE_0:def 3;
        hence thesis;
      end;
      UN = UN \/ X by A3,XBOOLE_1:7;
      hence thesis by A1,A2;
    end;
    hence thesis;
  end;

theorem
  not bool UN in UN by ZFMISC_1:def 1;

begin :: A sequence of universes

theorem Th88:
  for X being set
  ex f being Function st dom f = NAT & f.0 = X &
  for n being Nat holds f.(n+1) = GrothendieckUniverse (f.n)
  proof
    let X be set;
    deffunc G(set,set) = GrothendieckUniverse $2;
    ex f be Function st dom f = NAT & f.0 = X & for n be Nat holds
      f.(n+1) = G(n,f.n) from NAT_1:sch 11;
    hence thesis;
  end;

definition
  let X be set;
  func sequence_univers(X) -> Function means
:Def9:
  dom it = NAT & it.0 = X &
  for n be Nat holds it.(n+1) = GrothendieckUniverse (it.n);
  existence by Th88;
  uniqueness
  proof
    let f,g be Function such that
A1: dom f = NAT & f.0 = X &
    for n be Nat holds f.(n+1) = GrothendieckUniverse (f.n) and
A2: dom g = NAT & g.0 = X &
    for n be Nat holds g.(n+1) = GrothendieckUniverse (g.n);
    now
      thus dom f = dom g by A1,A2;
      defpred P[Nat] means (f.$1 = g.$1);

A3:   P[0] by A1,A2;
      now
        let k be Nat;
        assume
A4:     P[k];
        f.(k+1) = GrothendieckUniverse(f.k) by A1
               .= g.(k+1) by A4,A2;
        hence P[k+1];
      end;
      then
A5:   for k be Nat st P[k] holds P[k+1];
      for k be Nat holds P[k] from NAT_1:sch 2(A3,A5);
      hence for x be object st x in NAT holds f.x = g.x;
    end;
    hence thesis by A1,FUNCT_1:2;
  end;
end;

theorem
  for X being set holds sequence_univers X is Sequence
  proof
    let X be set;
    sequence_univers X is Sequence-like by Def9;
    hence thesis;
  end;

theorem Th90:
  for X being set for S being Sequence st dom S = NAT holds
  last S = S.NAT
  proof
    let X be set;
    let S be Sequence;
    assume dom S = NAT;
    then union dom S = NAT by ORDINAL1:def 6;
    hence thesis by ORDINAL2:def 1;
  end;

theorem Th91:
  for S being Sequence st dom S = NAT holds S.NAT = {} & last S = {}
  proof
    let S be Sequence;
    assume
A1: dom S = NAT;
    not NAT in NAT;
    hence S.NAT = {} by A1,FUNCT_1:def 2;
    hence thesis by A1,Th90;
  end;

theorem
  for X being set for S being Sequence st S = sequence_univers X holds
  last S = {} & S.NAT = {}
  proof
    let X be set;
    let S be Sequence;
    assume
A1: S = sequence_univers X;
    dom sequence_univers X = NAT by Def9;
    hence thesis by A1,Th91;
  end;

definition
  let X be set;
  func union_sequence_univers X -> non empty set equals
  union rng sequence_univers X;
  coherence
  proof
A1: dom sequence_univers X = NAT & (sequence_univers X).0 = X &
    for n be Nat holds (sequence_univers X).(n+1)
    = GrothendieckUniverse ((sequence_univers X).n) by Def9;
    set Y = (sequence_univers X).(0+1);
    Y = GrothendieckUniverse ((sequence_univers X).0) by Def9;
    then Y is non empty;
    then consider x be object such that
A2: x in Y;
    Y in rng sequence_univers X by A1,FUNCT_1:3;
    hence thesis by A2,TARSKI:def 4;
  end;
end;

theorem Th93:
  for X being set holds rng sequence_univers X c= union_sequence_univers X
  proof
    let X be set;
    now
      let x be object;
      assume x in rng sequence_univers X;
      then consider y be object such that
A1:   y in dom sequence_univers X and
A2:   x = (sequence_univers X).y by FUNCT_1:def 3;
      reconsider x9 = x as set by TARSKI:1;
      y in NAT by A1,Def9;
      then reconsider y as Nat;
      now
        (sequence_univers X).(y+1)
          = GrothendieckUniverse x9 by A2,Def9;
        hence x9 in (sequence_univers X).(y+1) by CLASSES3:def 4;
        y + 1 in NAT;
        then y + 1 in dom sequence_univers X by Def9;
        hence (sequence_univers X).(y+1) in rng sequence_univers X
          by FUNCT_1:3;
      end;
      hence x in union_sequence_univers X by TARSKI:def 4;
    end;
    hence thesis;
  end;

definition
  func sequence_univers -> sequence of union_sequence_univers {} equals
  sequence_univers {};
  coherence
  proof
    set SU = sequence_univers {};
    dom SU = NAT & rng SU c= union_sequence_univers {} &
      SU is Function of dom SU,rng SU by Th93,Def9,FUNCT_2:1;
    hence thesis by FUNCT_2:2;
  end;
end;

theorem Th94:
  {} in rng sequence_univers & FinSETS in rng sequence_univers &
  SETS in rng sequence_univers
  proof
    set f = sequence_univers {};
A1: dom f = NAT & f.0 = {} &
    for n be Nat holds f.(n+1) = GrothendieckUniverse (f.n) by Def9;
A2: f.1 = f.(0 + 1)
       .= GrothendieckUniverse ({}) by A1
       .=FinSETS by Th45,CLASSES2:56,CLASSES3:21;
    f.2 = f.(1 + 1)
       .= SETS by Th77,A2,Def9;
    hence thesis by A1,A2,FUNCT_1:3;
  end;

theorem
  not union rng sequence_univers is Grothendieck
  proof
    set RSU = rng sequence_univers,
        URSU = union RSU;
    assume URSU is Grothendieck;
    then reconsider URSU as non empty Grothendieck;
A1: URSU is axiom_GU1;
    set f = sequence_univers {};
    dom sequence_univers = NAT & rng sequence_univers c= URSU &
      NAT in URSU by A1,Th72,Th94,Def9;
    then URSU in URSU by CLASSES3:def 3;
    hence thesis;
  end;

theorem
  Tarski-Class FinSETS = GrothendieckUniverse FinSETS &
  Tarski-Class SETS = GrothendieckUniverse SETS
  by CLASSES3:22;

theorem
  for X being set for n being Nat holds
  (sequence_univers X).(n+1) is epsilon-transitive &
  Tarski-Class ((sequence_univers X).(n+1))
    = GrothendieckUniverse ((sequence_univers X).(n+1))
  proof
    let X be set;
    let n be Nat;
    (sequence_univers X).(n+1) = GrothendieckUniverse ((sequence_univers X).n)
      by Def9;
    hence thesis by CLASSES3:22;
  end;

theorem Th98:
  for n being Nat holds Tarski-Class ((sequence_univers FinSETS).n)
    = GrothendieckUniverse ((sequence_univers FinSETS).n)
  proof
    let n be Nat;
    per cases;
    suppose n = 0;
      then Tarski-Class ((sequence_univers FinSETS).n) = SETS &
        GrothendieckUniverse ((sequence_univers FinSETS).n) = SETS
        by Th77,Def9;
      hence thesis;
    end;
    suppose n <> 0;
      then consider m be Nat such that
A1:   n = m + 1 by NAT_1:6;
      (sequence_univers FinSETS).n
        = GrothendieckUniverse ((sequence_univers FinSETS).m) by A1,Def9;
      hence thesis by CLASSES3:22;
    end;
  end;

theorem Th99:
  for n being Nat holds UNIVERSE n in UNIVERSE (n+1)
  proof
    let n be Nat;
    succ Segm n = Segm(n + 1) by NAT_1:38;
    then UNIVERSE (n+1) = Tarski-Class (UNIVERSE n) by CLASSES2:66
                       .= GrothendieckUniverse (UNIVERSE n) by CLASSES3:22;
    hence thesis by CLASSES3:def 4;
  end;

theorem Th100:
  for n being Nat holds (sequence_univers FinSETS).n = UNIVERSE n
  proof
    let n be Nat;
    defpred P[Nat] means (sequence_univers FinSETS).$1 = UNIVERSE $1;
A1: P[0] by Def9,CLASSES2:65;
A2: for k be Nat st P[k] holds P[k+1]
    proof
      let k be Nat;
      assume
A3:  P[k];
      now
        thus (sequence_univers FinSETS).(k+1)
          = GrothendieckUniverse (sequence_univers FinSETS).k by Def9;
        succ Segm k = Segm(k + 1) by NAT_1:38;
        hence UNIVERSE (k+1)
          = Tarski-Class ((sequence_univers FinSETS).k) by A3,CLASSES2:66;
      end;
      hence thesis by Th98;
    end;
    for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
    hence thesis;
  end;

theorem Th101:
  for n being Nat holds
  GrothendieckUniverse((sequence_univers {}).n)
    = (sequence_univers GrothendieckUniverse {}).n
  proof
    defpred P[Nat] means GrothendieckUniverse ((sequence_univers {}).$1)
    = (sequence_univers GrothendieckUniverse {}).$1;

A1: P[0]
    proof
      GrothendieckUniverse ((sequence_univers {}).0)
        = GrothendieckUniverse {} &
      (sequence_univers GrothendieckUniverse {}).0 = GrothendieckUniverse {}
        by Def9;
      hence thesis;
    end;
A2: for k be Nat st P[k] holds P[k+1]
    proof
      let k be Nat;
      assume
A3:   P[k];
      GrothendieckUniverse ((sequence_univers {}).(k+1))
        = GrothendieckUniverse (GrothendieckUniverse (sequence_univers {}).k) &
      (sequence_univers GrothendieckUniverse {}).(k+1)
        = GrothendieckUniverse (sequence_univers (GrothendieckUniverse {})).k
        by Def9;
      hence thesis by A3;
    end;
    for k be Nat holds P[k] from NAT_1:sch 2 (A1,A2);
    hence thesis;
  end;

theorem Th102:
  for n being Nat holds sequence_univers.(n+1) = UNIVERSE n
  proof
    let n be Nat;
    sequence_univers.(n+1)
      = GrothendieckUniverse((sequence_univers {}).n) &
    UNIVERSE n
      = (sequence_univers GrothendieckUniverse {}).n by Th46,Th100,Def9;
    hence thesis by Th101;
  end;

registration
  cluster non empty for Element of union rng sequence_univers;
  existence by Th94;
end;

theorem Th103:
  FinSETS in GrothendieckUniverse sequence_univers &
  SETS in GrothendieckUniverse sequence_univers
  proof
    set SU = GrothendieckUniverse sequence_univers;
    now
      1 in NAT & 2 in NAT;
      hence 1 in dom sequence_univers & 2 in dom sequence_univers by Def9;
      set f = sequence_univers;
A1:   dom f = NAT & f.0 = {} &
        for n be Nat holds f.(n+1) = GrothendieckUniverse (f.n) by Def9;
      thus
A2:   f.1 = f.(0 + 1)
         .= GrothendieckUniverse ({}) by A1
         .=FinSETS by Th45,CLASSES2:56,CLASSES3:21;
      thus f.2 = f.(1 + 1)
              .= SETS by Th77,A2,Def9;
    end;
    then [1,FinSETS] in sequence_univers &
      [2,SETS] in sequence_univers & sequence_univers in SU &
      SU is axiom_GU1 by CLASSES3:def 4,FUNCT_1:1;
    then reconsider x = [1,FinSETS], y = [2,SETS] as pair Element of SU;
    x`2 is Element of SU & y`2 is Element of SU;
    hence thesis;
  end;

theorem Th104:
  for n being Nat holds
  (sequence_univers).(n+1) in GrothendieckUniverse sequence_univers
  proof
    let n be Nat;
    set SU = GrothendieckUniverse sequence_univers;
    now
      (n +1) in NAT;
      hence (n + 1) in dom sequence_univers by Def9;
      set f = sequence_univers;
A1:   dom f = NAT & f.0 = {} &
        for n be Nat holds f.(n+1) = GrothendieckUniverse (f.n) by Def9;
      thus f.1 = f.(0 + 1)
              .= GrothendieckUniverse ({}) by A1
              .= FinSETS by Th45,CLASSES2:56,CLASSES3:21;
    thus f.(n+1)=UNIVERSE n by Th102;
    end;
    then [(n + 1),(sequence_univers).(n + 1)] in sequence_univers &
      sequence_univers in SU & SU is axiom_GU1 by CLASSES3:def 4,FUNCT_1:1;
    then reconsider x = [(n+1),(sequence_univers).(n+1)] as pair Element of SU;
    x`2 is Element of SU;
    hence thesis;
  end;

definition
  func super_univers -> non trivial Universe equals
  GrothendieckUniverse sequence_univers;
  coherence
  proof
    set SU = GrothendieckUniverse sequence_univers;
    NAT in SETS & SETS in SU & SU is axiom_GU1 by Th103,Th72;
    hence thesis by Def6;
  end;
end;

theorem Th105:
  for n being Nat holds (sequence_univers).n c= (sequence_univers).(n+1)
  proof
    defpred P[Nat] means (sequence_univers).$1 c= (sequence_univers).($1+1);
A1: P[0]
    proof
      {} c= (sequence_univers).1;
      hence thesis by Def9;
    end;
A2: for k be Nat st P[k] holds P[k+1]
    proof
      let k be Nat;
      assume P[k];
A3:   (sequence_univers).(k+1) = UNIVERSE k by Th102;
      Segm k c= Segm (k + 1) by NAT_1:11,39;
      then UNIVERSE k c= UNIVERSE (k+1) by CLASSES2:72;
      hence thesis by A3,Th102;
    end;
    for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
    hence thesis;
  end;

definition
  let X being Element of union rng sequence_univers;
  func rank_univers X -> Nat means
:Def13:
  X in (sequence_univers).it &
  for n being Nat st n < it holds not X in (sequence_univers).n;
  existence
  proof
    consider Y be set such that
A1: X in Y and
A2: Y in rng sequence_univers {} by TARSKI:def 4;
    consider x be object such that
A3: x in dom sequence_univers {} and
A4: Y = (sequence_univers {}).x by A2,FUNCT_1:def 3;
    x in NAT by A3,Def9;
    then reconsider x as Nat;
    defpred P[Nat] means X in (sequence_univers).$1;
    X in (sequence_univers {}).x by A1,A4;
    then
A5: ex k be Nat st P[k];
    consider k be Nat such that
A6: P[k] and
A7: (for n be Nat st P[n] holds k <= n) from NAT_1:sch 5(A5);
    take k;
    thus thesis by A6,A7;
  end;
  uniqueness
  proof
    let n1,n2 be Nat such that
A8: X in (sequence_univers).n1 &
    for n be Nat st n < n1 holds not X in (sequence_univers).n and
A9: X in (sequence_univers).n2 &
    for n be Nat st n < n2 holds not X in (sequence_univers).n;
    n1 = n2
    proof
      assume n1 <> n2;
      then n1 < n2 or n2 < n1 by XXREAL_0:1;
      hence thesis by A8,A9;
    end;
    hence thesis;
  end;
end;

theorem
  for X being Element of union rng sequence_univers
  for n being Nat st rank_univers X <= n holds
  X in (sequence_univers).n
  proof
    let X be Element of union rng sequence_univers;
    let n be Nat;
    assume
A1: rank_univers X <= n;
    defpred P[Nat] means X in (sequence_univers).$1;
A2: P[rank_univers X] by Def13;
A3: for j be Nat st rank_univers X <= j & P[j] holds P[j+1]
    proof
      let j be Nat;
      assume that rank_univers X <= j and
A4:   P[j];
      (sequence_univers).j c= (sequence_univers).(j+1) by Th105;
      hence thesis by A4;
    end;
    for i be Nat st rank_univers X <= i holds P[i] from NAT_1:sch 8(A2,A3);
    hence thesis by A1;
  end;

theorem
  for i being Nat ex x being set st
  x in (sequence_univers).(i+1) \ (sequence_univers).i
  proof
    let i be Nat;
    assume for x be set holds
      not x in (sequence_univers).(i+1) \ (sequence_univers).i;
    then
A1: (sequence_univers).(i+1) \ (sequence_univers).i is empty;
    then
A2: (sequence_univers).(i+1) = (sequence_univers).i by Th105,XBOOLE_1:37;
    per cases;
    suppose
A3:   i = 0;
      GrothendieckUniverse (sequence_univers).0
        = (sequence_univers).(0+1) by Def9
       .= (sequence_univers).0 by A1,A3,Th105,XBOOLE_1:37
       .= {} by Def9;
      hence thesis;
    end;
    suppose i <> 0;
      then consider m be Nat such that
A4:   i = m + 1 by NAT_1:6;
A5:   sequence_univers.(i+1) = UNIVERSE i by Th102;
      sequence_univers.i = UNIVERSE m by A4,Th102;
      then m = i by A2,A5,CLASSES2:71;
      hence thesis by A4;
    end;
  end;

theorem
  for n being Nat holds not UNIVERSE (n + 1) \ UNIVERSE n in UNIVERSE(n + 1)
  proof
    let n be Nat;
    UNIVERSE n is Element of UNIVERSE(n+1) by Th99;
    hence thesis by Th86;
  end;

definition
  func ComplUniverse -> Function of NAT,union rng sequence_univers means
:Def14:
  for n being Nat holds it.n = UNIVERSE (n + 1) \ UNIVERSE n;
  existence
  proof
    deffunc F(Element of NAT) = UNIVERSE ($1 + 1) \ UNIVERSE $1;
    consider f be Function such that
A1: dom f = NAT and
A2: for n be Element of NAT st n in NAT holds f.n = F(n) from CLASSES1:sch 2;
    rng f c= union rng sequence_univers
    proof
      let x be object;
      assume x in rng f;
      then consider y be object such that
A3:   y in dom f and
A4:   x = f.y by FUNCT_1:def 3;
      reconsider y as Element of NAT by A1,A3;
A5:   UNIVERSE ((y + 1) + 1) is axiom_GU1;
A6:   UNIVERSE (y + 1) in UNIVERSE ((y + 1) + 1) by Th99;
      reconsider z1 = UNIVERSE (y + 1) as Element of UNIVERSE((y + 1) + 1)
        by Th99;
      UNIVERSE y in UNIVERSE (y + 1) by Th99;
      then reconsider z2 = UNIVERSE y as Element of UNIVERSE((y + 1) + 1)
        by A5,A6;
A7:   x = z1 \ z2 by A2,A4;
      UNIVERSE ((y + 1) + 1) in rng sequence_univers
      proof
        set n = (y + 1) + 1;
        n + 1 in NAT;
        then
A8:     n + 1 in dom sequence_univers by Def9;
        (sequence_univers).(n + 1) = UNIVERSE n by Th102;
        hence thesis by A8,FUNCT_1:def 3;
      end;
      hence thesis by A7,TARSKI:def 4;
    end;
    then reconsider f as Function of NAT,union rng sequence_univers
      by A1,FUNCT_2:2;
    take f;
    now
      let i be Nat;
      i is Element of NAT by ORDINAL1:def 12;
      hence f.i = UNIVERSE (i + 1) \ UNIVERSE i by A2;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f1,f2 be Function of NAT,union rng sequence_univers such that
A9: for n being Nat holds f1.n = UNIVERSE (n+1) \ UNIVERSE n and
A10: for n being Nat holds f2.n = UNIVERSE (n+1) \ UNIVERSE n;
    now
      let i be Element of NAT;
      reconsider i9 = i as Nat;
      f1.i9 = UNIVERSE (i9+1) \ UNIVERSE i9 by A9
           .= f2.i9 by A10;
      hence f1.i = f2.i;
    end;
    hence thesis;
  end;
end;

theorem Th109:
  for n being Nat holds ComplUniverse.n is non empty
  proof
    let n be Nat;
    assume ComplUniverse.n is empty;
    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 thesis;
  end;

theorem
  for n being Nat holds ComplUniverse.n c= UNIVERSE (n+1)
  proof
    let n be Nat;
    ComplUniverse.n = UNIVERSE (n + 1) \ UNIVERSE n by Def14;
    hence thesis;
  end;

theorem
  ex f being Function of NAT,union union rng sequence_univers st
  (for i being Nat holds f.i in ComplUniverse.i)
  proof
    set g = the Choice of ComplUniverse;
A1: dom g = dom ComplUniverse by ORDERS_1:def 1
         .= NAT by FUNCT_2:def 1;
    rng g c= union union rng sequence_univers
    proof
      let x be object;
      assume x in rng g;
      then consider y be object such that
A2:   y in dom g and
A3:   x = g.y by FUNCT_1:def 3;
      reconsider y as Element of NAT by A1,A2;
A4:   ComplUniverse.y is non empty by Th109;
      y in dom ComplUniverse by A1,A2,FUNCT_2:def 1;
      then x = the Element of ComplUniverse.y by A3,ORDERS_1:def 1;
      then
A5:  x in ComplUniverse.y by A4;
A6:  UNIVERSE ((y + 1) + 1) is axiom_GU1;
A7:   UNIVERSE (y + 1) in UNIVERSE ((y + 1) + 1) by Th99;
A8:   UNIVERSE ((y + 1) + 1) c= union rng sequence_univers
      proof
        let x be object;
        assume
A9:    x in UNIVERSE ((y + 1) + 1);
        set n = (y + 1) + 1;
        (n + 1) + 1 in NAT;
        then
A10:    ((n + 1) + 1) in dom sequence_univers by Def9;
A11:   x in (sequence_univers).(n + 1) &
         (sequence_univers).(n + 1) c= (sequence_univers).((n + 1) + 1)
         by Th102,A9,Th105;
        (sequence_univers).((n + 1) + 1) in rng sequence_univers
          by A10,FUNCT_1:def 3;
        hence thesis by A11,TARSKI:def 4;
      end;
      reconsider z1 = UNIVERSE (y + 1) as Element of UNIVERSE((y + 1) + 1)
        by Th99;
      UNIVERSE y in UNIVERSE (y + 1) by Th99;
      then reconsider z2 = UNIVERSE y as Element of UNIVERSE((y + 1) + 1)
        by A6,A7;
A12:   x in z1 \ z2 by A5,Def14;
      x in union UNIVERSE ((y+1)+1) &
      union UNIVERSE ((y+1)+1) c= union union rng sequence_univers
        by A12,A8,ZFMISC_1:77,TARSKI:def 4;
      hence thesis;
    end;
    then reconsider g as Function of NAT,union union rng sequence_univers
      by A1,FUNCT_2:2;
    take g;
    for i be Nat holds g.i in ComplUniverse.i
    proof
      let i be Nat;
      dom ComplUniverse = NAT by FUNCT_2:def 1;
      then g.i = the Element of (ComplUniverse).i
        by ORDERS_1:def 1,ORDINAL1:def 12;
      then g.i is Element of (ComplUniverse).i & ComplUniverse.i is non empty
        by Th109;
      hence thesis;
    end;
    hence thesis;
  end;

theorem
  for f being Function of NAT,union rng sequence_univers holds
  f in super_univers
  proof
    let f be Function of NAT,union rng sequence_univers;
A1: super_univers is non trivial;
    now
      dom sequence_univers = NAT & super_univers is non trivial by Def9;
      hence dom sequence_univers in super_univers;
      now
        let x be object;
        assume x in rng sequence_univers;
        then consider y be object such that
A2:     y in dom sequence_univers and
A3:     x = (sequence_univers).y by FUNCT_1:def 3;
        reconsider y as Nat by A2;
        per cases;
        suppose
A4:       y = 0;
          (sequence_univers).0 = {} by Def9;
          hence x in super_univers by A4,A3,Th13;
        end;
        suppose y <> 0;
          then consider m be Nat such that
A5:       y = m + 1 by NAT_1:6;
          thus x in super_univers by A5,A3,Th104;
        end;
      end;
      hence rng sequence_univers c= super_univers;
    end;
    then union rng sequence_univers in super_univers by CLASSES3:def 3;
    then [:NAT,union rng sequence_univers:] in super_univers by A1,CLASSES2:61;
    hence thesis by Th13;
  end;

theorem
  for f being Function of NAT,union union rng sequence_univers holds
  f in super_univers
  proof
    let f be Function of NAT,union union rng sequence_univers;
A1: super_univers is non trivial;
    now
      dom sequence_univers = NAT & super_univers is non trivial by Def9;
      hence dom sequence_univers in super_univers;
      now
        let x be object;
        assume x in rng sequence_univers;
        then consider y be object such that
A2:     y in dom sequence_univers and
A3:     x = (sequence_univers).y by FUNCT_1:def 3;
        reconsider y as Nat by A2;
        per cases;
        suppose
A4:       y = 0;
          (sequence_univers).0 = {} by Def9;
          hence x in super_univers by A4,A3,Th13;
        end;
        suppose y <> 0;
          then ex m be Nat st y = m + 1 by NAT_1:6;
          hence x in super_univers by A3,Th104;
        end;
      end;
      hence rng sequence_univers c= super_univers;
    end;
    then union rng sequence_univers in super_univers by CLASSES3:def 3;
    then union union rng sequence_univers in super_univers by CLASSES2:59;
    then [:NAT,union union rng sequence_univers:] in super_univers
      by A1,CLASSES2:61;
    hence thesis by Th13;
  end;