:: Mostowski's Fundamental Operations - Part II
::  by Grzegorz Bancerek and Andrzej Kondracki
::
:: Received February 15, 1991
:: Copyright (c) 1991-2012 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 NUMBERS, ZF_LANG, XBOOLE_0, SUBSET_1, FUNCT_1, ARYTM_3, CARD_1,
      ZF_MODEL, TARSKI, ORDINAL1, BVFUNC_2, XBOOLEAN, ZFMISC_1, CLASSES2,
      ZF_REFLE, CARD_3, RELAT_1, ORDINAL2, ZF_LANG1, ZFMODEL1, XXREAL_0,
      REALSET1, ZF_FUND1, FUNCT_2, ORDINAL4, NAT_1, ZF_FUND2;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, NUMBERS,
      ORDINAL1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ZF_LANG,
      ZF_MODEL, ZFMODEL1, ORDINAL2, CARD_3, ZF_LANG1, CLASSES2, ORDINAL4,
      ZF_REFLE, ZF_FUND1, XXREAL_0;
 constructors PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, CLASSES1,
      ZFMODEL1, ZF_LANG1, ZF_REFLE, ZF_FUND1, ORDINAL4, RELSET_1, ZF_MODEL;
 registrations ORDINAL1, RELSET_1, FINSET_1, XREAL_0, CARD_1, CLASSES2,
      ZF_LANG, ORDINAL4, FUNCT_1, ZF_FUND1, ZF_LANG1;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, ORDINAL1, XBOOLE_0;
 theorems TARSKI, NAT_1, ENUMSET1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2,
      CARD_1, ZF_MODEL, ZFMODEL1, ZFMODEL2, ZF_LANG1, CARD_3, ZF_REFLE,
      ZFREFLE1, CLASSES2, ZFMISC_1, ZF_FUND1, GRFUNC_1, RELAT_1, CLASSES1,
      RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, FUNCT_7;
 schemes ZF_REFLE, NAT_1;

begin

reserve H for ZF-formula,
  M,E for non empty set,
  e for Element of E,
  m,m0,m3, m4 for Element of M,
  v,v1,v2 for Function of VAR,M,
  f,f1 for Function of VAR,E,
  g for Function,
  u,u1,u2 for set,
  x,y for Variable,
  i,n for Element of NAT,
  X for set;

definition
  let H,M,v;
  func Section(H,v) -> Subset of M equals
  : Def1:
  { m : M,v/(x.0,m) |= H } if
  x.0 in Free H otherwise {};
  coherence
  proof
    thus x.0 in Free H implies { m where m is Element of M: M,v/(x.0,m) |= H }
    is Subset of M
    proof
      set X = {m where m is Element of M: M,v/(x.0,m) |= H };
      assume x.0 in Free H;
      X c= M
      proof
        let u;
        assume u in X;
        then ex m being Element of M st u = m & M,v/(x.0,m) |= H;
        hence thesis;
      end;
      hence thesis;
    end;
    thus thesis by XBOOLE_1:2;
  end;
  consistency;
end;

definition
  let M;
  attr M is predicatively_closed means
  : Def2:
  for H, E, f st E in M holds Section(H,f) in M;
end;

theorem Th1:
  E is epsilon-transitive implies Section(All(x.2,x.2 'in' x.0 =>
  x.2 'in' x.1),f/(x.1,e)) = E /\ bool e
proof
  set H = All(x.2,x.2 'in' x.0 => x.2 'in' x.1), v = f/(x.1,e);
  set S = Section(H,v);
  Free H=Free(x.2 'in' x.0 => x.2 'in' x.1)\{x.2} by ZF_LANG1:62
    .=(Free(x.2 'in' x.0) \/ Free(x.2 'in' x.1))\{x.2} by ZF_LANG1:64
    .=(Free(x.2 'in' x.0) \/ {x.2,x.1})\{x.2} by ZF_LANG1:59
    .=({x.2,x.0} \/ {x.2,x.1})\{x.2} by ZF_LANG1:59
    .=({x.2,x.0}\{x.2}) \/ ({x.2,x.1}\{x.2}) by XBOOLE_1:42
    .=({x.2,x.0}\{x.2}) \/ {x.1} by ZFMISC_1:17,ZF_LANG1:76
    .={x.0} \/ {x.1} by ZFMISC_1:17,ZF_LANG1:76
    .={x.0,x.1} by ENUMSET1:1;
  then x.0 in Free H by TARSKI:def 2;
  then
A1: S={m where m is Element of E: E,v/(x.0,m)|= H} by Def1;
  assume
A2: X in E implies X c= E;
  thus S c= E /\ bool e
  proof
    let u;
    assume u in S;
    then consider m being Element of E such that
A3: u = m and
A4: E,v/(x.0,m) |= H by A1;
A5: m c= E by A2;
    m c= e
    proof
      let u1;
      assume
A6:   u1 in m;
      then reconsider u1 as Element of E by A5;
A7:   v/(x.0,m)/(x.2,u1).(x.2) = u1 by FUNCT_7:128;
A8:   E,v/(x.0,m)/(x.2,u1) |= x.2 'in' x.0 => x.2 'in' x.1 by A4,ZF_LANG1:71;
A9:   v/(x.0,m)/(x.2,u1).(x.1) = v/(x.0,m).(x.1) & v.(x.1) = v/(x.0,m).(
      x.1) by FUNCT_7:32,ZF_LANG1:76;
      m = v/(x.0,m).(x.0) & v/(x.0,m)/(x.2,u1).(x.0) = v/(x.0,m).(x.0) by
FUNCT_7:32,128,ZF_LANG1:76;
      then E,v/(x.0,m)/(x.2,u1) |= x.2 'in' x.0 by A6,A7,ZF_MODEL:13;
      then v.x.1 = e & E,v/(x.0,m)/(x.2,u1) |= x.2 'in' x.1 by A8,FUNCT_7:128
,ZF_MODEL:18;
      hence thesis by A7,A9,ZF_MODEL:13;
    end;
    then u in bool e by A3,ZFMISC_1:def 1;
    hence thesis by A3,XBOOLE_0:def 4;
  end;
  let u;
  assume
A10: u in E /\ bool e;
  then
A11: u in bool e by XBOOLE_0:def 4;
  reconsider u as Element of E by A10,XBOOLE_0:def 4;
  now
A12: v.x.1 = e by FUNCT_7:128;
    let m be Element of E;
A13: v/(x.0,u)/(x.2,m).(x.2) = m by FUNCT_7:128;
A14: u = v/(x.0,u).(x.0) & v/(x.0,u)/(x.2,m).(x.0) = v/(x.0,u).(x.0) by
FUNCT_7:32,128,ZF_LANG1:76;
A15: v/(x.0,u)/(x.2,m).(x.1) = v/(x.0,u).(x.1) & v.(x.1) = v/(x.0,u).(x.1)
    by FUNCT_7:32,ZF_LANG1:76;
    now
      assume E,v/(x.0,u)/(x.2,m) |= x.2 'in' x.0;
      then m in u by A13,A14,ZF_MODEL:13;
      hence E,v/(x.0,u)/(x.2,m) |= x.2 'in' x.1 by A11,A13,A15,A12,ZF_MODEL:13;
    end;
    hence E,v/(x.0,u)/(x.2,m) |= x.2 'in' x.0 => x.2 'in' x.1 by ZF_MODEL:18;
  end;
  then E,v/(x.0,u) |= H by ZF_LANG1:71;
  hence thesis by A1;
end;

reserve W for Universe,
  w for Element of W,
  Y for Subclass of W,
  a,a1,b,c for Ordinal of W,
  L for DOMAIN-Sequence of W;

Lm1: u1 in Union g implies ex u2 st u2 in dom g & u1 in g.u2
proof
  assume u1 in Union g;
  then u1 in union rng g by CARD_3:def 4;
  then consider X such that
A1: u1 in X and
A2: X in rng g by TARSKI:def 4;
  consider u2 such that
A3: u2 in dom g & X = g.u2 by A2,FUNCT_1:def 3;
  take u2;
  thus thesis by A1,A3;
end;

theorem Th2:
  (for a,b st a in b holds L.a c= L.b) & (for a holds L.a in Union
L & L.a is epsilon-transitive) & Union L is predicatively_closed implies Union
  L |= the_axiom_of_power_sets
proof
  assume that
A1: for a,b st a in b holds L.a c= L.b and
A2: for a holds L.a in Union L & L.a is epsilon-transitive and
A3: Union L is predicatively_closed;
  set M = Union L;
A4: X in L.a implies L.a /\ bool X in M
  proof
    set f = the Function of VAR,L.a;
    assume X in L.a;
    then reconsider e = X as Element of L.a;
    L.a in M by A2;
    then
A5: Section(All(x.2,x.2 'in' x.0 => x.2 'in' x.1),f/(x.1,e)) in M by A3,Def2;
    L.a is epsilon-transitive by A2;
    hence thesis by A5,Th1;
  end;
A6: now
    defpred P[set,set] means $1 in L.$2;
    let X such that
A7: X in M;
A8: X in bool X by ZFMISC_1:def 1;
    then reconsider D = M /\ bool X as non empty set by A7,XBOOLE_0:def 4;
A9: X in M /\ bool X by A7,A8,XBOOLE_0:def 4;
A10: for d being Element of D ex a st P[d,a]
    proof
      let d be Element of D;
      d in M by XBOOLE_0:def 4;
      then consider u2 such that
A11:  u2 in dom L and
A12:  d in L.u2 by Lm1;
      u2 in On W by A11,ZF_REFLE:def 2;
      then reconsider u2 as Ordinal of W by ZF_REFLE:7;
      take u2;
      thus thesis by A12;
    end;
    consider f being Function such that
A13: dom f = D & for d being Element of D ex a st a = f.d & P[d,a] &
    for b st P[d,b] holds a c= b from ZF_REFLE:sch 1(A10);
A14: rng f c= W
    proof
      let u;
      assume u in rng f;
      then consider u1 such that
A15:  u1 in D and
A16:  u = f.u1 by A13,FUNCT_1:def 3;
      reconsider u1 as Element of D by A15;
      ex a st a = f.u1 & u1 in L.a & for b st u1 in L.b holds a c= b by A13;
      hence thesis by A16;
    end;
A17: M /\ bool X c= bool X by XBOOLE_1:17;
    bool X in W by A7,CLASSES2:59;
    then D in W by A17,CLASSES1:def 1;
    then rng f = f.:(dom f) & card D in card W by CLASSES2:1,RELAT_1:113;
    then card rng f in card W by A13,CARD_1:67,ORDINAL1:12;
    then rng f in W by A14,CLASSES1:1;
    then reconsider a = sup rng f as Ordinal of W by ZF_REFLE:19;
A18: D c= L.a
    proof
      let u2;
      assume u2 in D;
      then reconsider d = u2 as Element of D;
      consider c such that
A19:  c = f.d and
A20:  d in L.c and
      for b st d in L.b holds c c= b by A13;
      c in rng f by A13,A19,FUNCT_1:def 3;
      then L.c c= L.a by A1,ORDINAL2:19;
      hence thesis by A20;
    end;
A21: L.a /\ bool X c= D by XBOOLE_1:26,ZF_REFLE:16;
    D /\ bool X = M /\ (bool X /\ bool X) by XBOOLE_1:16;
    then D c= L.a /\ bool X by A18,XBOOLE_1:26;
    then D = L.a /\ bool X by A21,XBOOLE_0:def 10;
    hence M /\ bool X in M by A4,A9,A18;
  end;
  Union L is epsilon-transitive
  proof
    let X;
    assume X in Union L;
    then consider u such that
A22: u in dom L and
A23: X in L.u by Lm1;
    reconsider u as Ordinal by A22;
    u in On W by A22,ZF_REFLE:def 2;
    then reconsider u as Ordinal of W by ZF_REFLE:7;
    L.u is epsilon-transitive by A2;
    then
A24: X c= L.u by A23,ORDINAL1:def 2;
    let u1;
A25: L.u c= Union L by ZF_REFLE:16;
    assume u1 in X;
    then u1 in L.u by A24;
    hence thesis by A25;
  end;
  hence thesis by A6,ZFMODEL1:9;
end;

Lm2: not x in variables_in H & {x.0,x.1,x.2} misses Free H & M,v |= All(x.3,Ex
(x.0,All(x.4,H <=> x.4 '=' x.0))) implies {x.0,x.1,x.2} misses Free (H/(x.0,x))
& M,v |= All(x.3,Ex(x.0,All(x.4,H/(x.0,x) <=> x.4 '=' x.0))) & def_func'(H,v) =
def_func'(H/(x.0,x),v)
proof
  assume that
A1: not x in variables_in H and
A2: {x.0,x.1,x.2} misses Free H and
A3: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
  x.0 in {x.0,x.1,x.2} by ENUMSET1:def 1;
  then
A4: not x.0 in Free H by A2,XBOOLE_0:3;
  hence {x.0,x.1,x.2} misses Free (H/(x.0,x)) by A1,A2,ZFMODEL2:2;
A5: not x.0 in Free (H/(x.0,x)) by A1,A4,ZFMODEL2:2;
A6: now
    let m3 be Element of M;
    consider m0 being Element of M such that
A7: M,v/(x.3,m3)/(x.4,m) |= H iff m = m0 by A3,A4,ZFMODEL2:19;
    take m0;
    let m4 be Element of M;
    thus M,v/(x.3,m3)/(x.4,m4) |= H/(x.0,x) implies m4 = m0
    proof
      assume M,v/(x.3,m3)/(x.4,m4) |= H/(x.0,x);
      then M,v/(x.3,m3)/(x.4,m4)/(x.0,v/(x.3,m3)/(x.4,m4).x) |= H by A1,
ZFMODEL2:12;
      then M,v/(x.3,m3)/(x.4,m4) |= H by A4,ZFMODEL2:9;
      hence thesis by A7;
    end;
    assume m4 = m0;
    then M,v/(x.3,m3)/(x.4,m4) |= H by A7;
    then M,v/(x.3,m3)/(x.4,m4)/(x.0,v/(x.3,m3)/(x.4,m4).x) |= H by A4,
ZFMODEL2:9;
    hence M,v/(x.3,m3)/(x.4,m4) |= H/(x.0,x) by A1,ZFMODEL2:12;
  end;
  Free H = Free (H/(x.0,x)) by A1,A4,ZFMODEL2:2;
  hence
A8: M,v |= All(x.3,Ex(x.0,All(x.4,H/(x.0,x) <=> x.4 '=' x.0))) by A4,A6,
ZFMODEL2:19;
  now
    let u;
    assume u in M;
    then reconsider u9 = u as Element of M;
    set m = def_func'(H,v).u9;
    M,v/(x.3,u9)/(x.4,m) |= H by A3,A4,ZFMODEL2:10;
    then M,v/(x.3,u9)/(x.4,m)/(x.0,v/(x.3,u9)/(x.4,m).x) |= H by A4,ZFMODEL2:9
;
    then M,v/(x.3,u9)/(x.4,m) |= H/(x.0,x) by A1,ZFMODEL2:12;
    hence def_func'(H,v).u = def_func'(H/(x.0,x),v).u by A5,A8,ZFMODEL2:10;
  end;
  hence thesis by FUNCT_2:12;
end;

Lm3: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) & not x.4 in Free H
implies for m holds def_func'(H,v).:m={}
proof
  set m3 = the Element of M;
  assume that
A1: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) and
A2: not x.4 in Free H;
  M,v/(x.3,m3) |= Ex(x.0,All(x.4,H <=> x.4 '=' x.0)) by A1,ZF_LANG1:71;
  then consider m0 such that
A3: M,v/(x.3,m3)/(x.0,m0) |= All(x.4,H <=> x.4 '=' x.0) by ZF_LANG1:73;
  let m;
  set u = the Element of def_func'(H,v).:m;
  assume def_func'(H,v).:m<>{};
  then consider u1 such that
A4: u1 in dom def_func'(H,v) and
A5: u1 in m and
  u=def_func'(H,v).u1 by FUNCT_1:def 6;
  set f=v/(x.3,m3)/(x.0,m0);
  reconsider u1 as Element of M by A4;
A6: now
    let m4;
    M,f/(x.4,m4) |= H <=> x.4 '=' x.0 by A3,ZF_LANG1:71;
    then M,f/(x.4,m4) |= H iff M,f/(x.4,m4) |= x.4 '=' x.0 by ZF_MODEL:19;
    then
A7: M,f |= H iff f/(x.4,m4).x.4=f/(x.4,m4).x.0 by A2,ZFMODEL2:9,ZF_MODEL:12;
    f/(x.4,m4).x.4=m4 & f.x.0=m0 by FUNCT_7:128;
    hence M,f |= H iff m4=m0 by A7,FUNCT_7:32,ZF_LANG1:76;
  end;
  then M,f |= H;
  then u1=m0 & m=m0 by A6;
  hence contradiction by A5;
end;

Lm4: not y in variables_in H & x<>x.0 & y<>x.0 & y<>x.4 implies (x.4 in Free H
iff x.0 in Free(Ex(x.3,x.3 'in' x '&' (H/(x.0,y)/(x.4,x.0)))))
proof
A1: x.0<>x.3 by ZF_LANG1:76;
  assume that
A2: not y in variables_in H and
A3: x<>x.0 and
A4: y<>x.0 and
A5: y<>x.4;
  set G=H/(x.0,y)/(x.4,x.0);
A6: Free(Ex(x.3,x.3 'in' x '&' G))= Free(x.3 'in' x '&' G)\{x.3} by ZF_LANG1:66
    .=(Free(x.3 'in' x) \/ Free(G))\{x.3} by ZF_LANG1:61
    .=({x.3,x} \/ Free(G))\{x.3} by ZF_LANG1:59
    .=({x.3,x}\{x.3}) \/ (Free(G)\{x.3}) by XBOOLE_1:42;
A7: x.0<>x.4 by ZF_LANG1:76;
A8: now
    assume
A9: x.4 in Free H;
A10: x.4 in Free(H/(x.0,y))
    proof
      now
        per cases;
        suppose
A11:      x.0 in Free H;
          not x.4 in {x.0} by A7,TARSKI:def 1;
          then
A12:      x.4 in Free H \ {x.0} by A9,XBOOLE_0:def 5;
          Free(H/(x.0,y))=(Free H \{x.0}) \/ {y} by A2,A11,ZFMODEL2:2;
          hence thesis by A12,XBOOLE_0:def 3;
        end;
        suppose
          not x.0 in Free H;
          hence thesis by A2,A9,ZFMODEL2:2;
        end;
      end;
      hence thesis;
    end;
A13: x.0 in {x.0} by TARSKI:def 1;
    not x.0 in variables_in(H/(x.0,y)) by A4,ZF_LANG1:184;
    then Free G=(Free(H/(x.0,y))\{x.4}) \/ {x.0} by A10,ZFMODEL2:2;
    then
A14: x.0 in Free G by A13,XBOOLE_0:def 3;
    not x.0 in {x.3} by A1,TARSKI:def 1;
    then x.0 in Free(G)\{x.3} by A14,XBOOLE_0:def 5;
    hence x.0 in Free(Ex(x.3,x.3 'in' x '&' G)) by A6,XBOOLE_0:def 3;
  end;
  now
    assume x.0 in Free(Ex(x.3,x.3 'in' x '&' G));
    then x.0 in {x.3,x}\{x.3} or x.0 in Free(G)\{x.3} by A6,XBOOLE_0:def 3;
    then
A15: x.0 in {x.3,x} or x.0 in Free G by XBOOLE_0:def 5;
A16: not x.0 in variables_in(H/(x.0,y)) by A4,ZF_LANG1:184;
A17: now
      assume not x.4 in Free(H/(x.0,y));
      then
A18:  x.0 in Free(H/(x.0,y)) by A3,A1,A15,A16,TARSKI:def 2,ZFMODEL2:2;
      Free(H/(x.0,y)) c= variables_in(H/(x.0,y)) by ZF_LANG1:151;
      hence contradiction by A4,A18,ZF_LANG1:184;
    end;
    Free(H/(x.0,y)) c= (Free H \ {x.0}) \/ {y} by ZFMODEL2:1;
    then x.4 in Free H \ {x.0} or x.4 in {y} by A17,XBOOLE_0:def 3;
    hence x.4 in Free H by A5,TARSKI:def 1,XBOOLE_0:def 5;
  end;
  hence thesis by A8;
end;

theorem Th3:
  omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a
<> {} & a is limit_ordinal holds L.a = Union (L|a)) & (for a holds L.a in Union
L & L.a is epsilon-transitive) & Union L is predicatively_closed implies for H
st {x.0,x.1,x.2} misses Free H holds Union L |= the_axiom_of_substitution_for H
proof
  assume that
A1: omega in W and
A2: for a,b st a in b holds L.a c= L.b and
A3: for a st a <> {} & a is limit_ordinal holds L.a = Union (L|a) and
A4: for a holds L.a in Union L & L.a is epsilon-transitive and
A5: Union L is predicatively_closed;
  set M = Union L;
A6: now
    defpred P[set,set] means $1 in L.$2;
    let H;
    let f be Function of VAR,M such that
A7: {x.0,x.1,x.2} misses Free H and
A8: M,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
    consider k being Element of NAT such that
A9: for i st x.i in variables_in H holds i < k by ZFMODEL2:3;
    set p = H/(x.0,x.(k+5));
    k+0 = k;
    then
A10: not x.(k+5) in variables_in H by A9,XREAL_1:7;
    then
A11: M,f |= All(x.3,Ex(x.0,All(x.4,p <=> x.4 '=' x.0))) & def_func'(H,f) =
    def_func'(p,f) by A7,A8,Lm2;
    set F = def_func'(H,f);
A12: for d being Element of M qua non empty set ex a st P[d,a]
    proof
      let d be Element of M qua non empty set;
      consider u such that
A13:  u in dom L and
A14:  d in L.u by Lm1;
      u in On W by A13,ZF_REFLE:def 2;
      then reconsider u as Ordinal of W by ZF_REFLE:7;
      take u;
      thus thesis by A14;
    end;
    consider g being Function such that
A15: dom g = M & for d being Element of M qua non empty set ex a st a
    = g.d & P[d,a] & for b st P[d,b] holds a c= b from ZF_REFLE:sch 1(A12);
A16: rng g c= W
    proof
      let u1;
      assume u1 in rng g;
      then consider u2 such that
A17:  u2 in dom g and
A18:  u1 = g.u2 by FUNCT_1:def 3;
      reconsider d = u2 as Element of M by A15,A17;
      ex a st a = g.d & d in L.a & for b st d in L.b holds a c= b by A15;
      hence thesis by A18;
    end;
    card VAR = omega & omega in card W by A1,CARD_1:5,47,CLASSES2:1,ZF_REFLE:17
;
    then
A19: card dom f in card W by FUNCT_2:def 1;
    rng f = f.: dom f by RELAT_1:113;
    then card (rng f) in card W by A19,CARD_1:67,ORDINAL1:12;
    then
A20: card (g.:(rng f)) in card W by CARD_1:67,ORDINAL1:12;
    g.:(rng f) c= rng g by RELAT_1:111;
    then g.:(rng f) c= W by A16,XBOOLE_1:1;
    then g.:(rng f) in W by A20,CLASSES1:1;
    then reconsider b2 = sup (g.:(rng f)) as Ordinal of W by ZF_REFLE:19;
A21: x.0 in {x.0,x.1,x.2} by ENUMSET1:def 1;
    {x.0,x.1,x.2} misses Free p by A7,A8,A10,Lm2;
    then
A22: not x.0 in Free p by A21,XBOOLE_0:3;
A23: X c= M & sup (g.:X) c= a implies X c= L.a
    proof
      assume that
A24:  X c= M and
A25:  sup (g.:X) c= a;
      let u1;
      assume
A26:  u1 in X;
      then reconsider d = u1 as Element of M by A24;
      consider b such that
A27:  b = g.d and
A28:  d in L.b and
      for a st d in L.a holds b c= a by A15;
      b in g.:X by A15,A26,A27,FUNCT_1:def 6;
      then b in sup (g.:X) by ORDINAL2:19;
      then L.b c= L.a by A2,A25;
      hence thesis by A28;
    end;
    let u be Element of M;
    consider b0 being Ordinal of W such that
    b0 = g.u and
A29: u in L.b0 and
    for b st u in L.b holds b0 c= b by A15;
A30: card u in card W by CLASSES2:1;
    k+0 = k;
    then
A31: 0 <= k & k < k+5 by NAT_1:2,XREAL_1:6;
    then
A32: not x.0 in variables_in p by ZF_LANG1:76,184;
    g.:(F.:u) c= rng g by RELAT_1:111;
    then
A33: g.:(F.:u) c= W by A16,XBOOLE_1:1;
    card (g.:(F.:u)) c= card (F.:u) & card (F.:u) c= card u by CARD_1:67;
    then card (g.:(F.:u)) in card W by A30,ORDINAL1:12,XBOOLE_1:1;
    then g.:(F.:u) in W by A33,CLASSES1:1;
    then reconsider b1 = sup (g.:(F.:u)) as Ordinal of W by ZF_REFLE:19;
    set b = b0 \/ b1;
    set a = b \/ b2;
A34: F.:u c= L.b by A23,XBOOLE_1:7;
    consider phi being Ordinal-Sequence of W such that
A35: phi is increasing & phi is continuous and
A36: for a st phi.a = a & {} <> a for v being Function of VAR,L.a
holds M,M!v |= p/(x.4,x.0) iff L.a,v |= p/(x.4,x.0) by A1,A2,A3,ZF_REFLE:20;
    consider a1 such that
A37: a in a1 and
A38: phi.a1 = a1 by A1,A35,ZFREFLE1:28;
A39: rng f c= L.a1
    proof
      let u;
A40:  b2 c= a by XBOOLE_1:7;
      assume
A41:  u in rng f;
      then consider u1 such that
A42:  u1 in dom f and
A43:  u = f.u1 by FUNCT_1:def 3;
      reconsider u1 as Variable by A42;
      consider a2 being Ordinal of W such that
A44:  a2 = g.(f.u1) and
A45:  f.u1 in L.a2 and
      for b st f.u1 in L.b holds a2 c= b by A15;
      a2 in g.:rng f by A15,A41,A43,A44,FUNCT_1:def 6;
      then a2 in b2 by ORDINAL2:19;
      then L.a2 c= L.a1 by A2,A37,A40,ORDINAL1:10;
      hence thesis by A43,A45;
    end;
    set x = x.(k+10);
    k+0 = k;
    then not k+10 < k by XREAL_1:6;
    then not x in variables_in H by A9;
    then
A46: not x in variables_in H \ {x.0} by XBOOLE_0:def 5;
    set q = Ex(x.3,x.3 'in' x '&' (p/(x.4,x.0)));
A47: 10 <= 10+k by NAT_1:11;
    b0 c= b & b c= a by XBOOLE_1:7;
    then b0 c= a by XBOOLE_1:1;
    then
A48: L.b0 c= L.a1 by A2,A37,ORDINAL1:12;
    then reconsider mu = u as Element of L.a1 by A29;
    dom f = VAR by FUNCT_2:def 1;
    then reconsider v = f as Function of VAR,L.a1 by A39,FUNCT_2:def 1
,RELSET_1:4;
    set w = v/(x.0,v.x.4)/(x,mu);
A49: x <> x.(k+5) implies not x in {x.(k+5)} by TARSKI:def 1;
    variables_in p c= (variables_in H \ {x.0}) \/ {x.(k+5)} & k+5 <> k+
    10 by ZF_LANG1:187;
    then not x in variables_in p by A46,A49,XBOOLE_0:def 3,ZF_LANG1:76;
    then
A50: variables_in (p/(x.4,x.0)) c= (variables_in p \ {x.4}) \/ {x.0} &
    not x in variables_in p \ {x.4} by XBOOLE_0:def 5,ZF_LANG1:187;
A51: 10 > 0;
    then
A52: x <> x.0 by A47,ZF_LANG1:76;
    then not x in {x.0} by TARSKI:def 1;
    then
A53: not x in variables_in (p/(x.4,x.0)) by A50,XBOOLE_0:def 3;
A54: 10 > 3;
    then
A55: x.0 <> x.3 & x <> x.3 by A47,ZF_LANG1:76;
    b in a1 by A37,ORDINAL1:12,XBOOLE_1:7;
    then L.b c= L.a1 by A2;
    then
A56: F.:u c= L.a1 by A34,XBOOLE_1:1;
A57: F.:u = Section(q,w)
    proof
      now
        per cases;
        suppose
A58:      x.4 in Free H;
          4<>k+5 by NAT_1:11;
          then
A59:      x.(k+5)<>x.4 by ZF_LANG1:76;
A60:      x.(k+10)<>x.0 by A51,A47,ZF_LANG1:76;
          ( not x.(k+5) in variables_in H)& x.(k+5)<>x.0 by A9,A31,ZF_LANG1:76;
          then
A61:      x.0 in Free q by A58,A60,A59,Lm4;
A62:      F.:u c= Section(q,w)
          proof
            let u1;
            assume
A63:        u1 in F.:u;
            then consider u2 such that
A64:        u2 in dom F and
A65:        u2 in u and
A66:        u1 = F.u2 by FUNCT_1:def 6;
            reconsider m1 = u1 as Element of L.a1 by A56,A63;
            reconsider u2 as Element of M by A64;
            L.a1 is epsilon-transitive by A4;
            then u c= L.a1 by A29,A48,ORDINAL1:def 2;
            then reconsider m2 = u2 as Element of L.a1 by A65;
A67:        f/(x.3,u2)/(x.0,F.u2) = M!(v/(x.3,m2)/(x.0,m1)) by A66,
ZF_LANG1:def 1,ZF_REFLE:16;
            M,f/(x.3,u2)/(x.4,F.u2) |= p & f/(x.3,u2)/(x.4,F.u2).(x.4)=F
            . u2 by A11,A22,FUNCT_7:128,ZFMODEL2:10;
            then M,f/(x.3,u2)/(x.4,F.u2)/(x.0,F.u2) |= p/(x.4,x.0) by A32,
ZFMODEL2:13;
            then
A68:        M,f/(x.3,u2)/(x.0,F.u2)/(x.4,F.u2) |= p/(x.4,x.0) by FUNCT_7:33
,ZF_LANG1:76;
            not x.4 in variables_in (p/(x.4,x.0)) by ZF_LANG1:76,184;
            then M,f/(x.3,u2)/(x.0,F.u2) |= p/(x.4,x.0) by A68,ZFMODEL2:5;
            then L.a1,v/(x.3,m2)/(x.0,m1) |= p/(x.4,x.0) by A36,A37,A38,A67;
            then
A69:        L.a1,v/(x.3,m2)/(x.0,m1)/(x,mu) |= p/(x.4,x.0) by A53,ZFMODEL2:5;
A70:        w.x = w/(x.0,m1).x & w.x = mu by A51,A47,FUNCT_7:32,128,ZF_LANG1:76
;
            w/(x.0,m1)/(x.3,m2).(x.3) = m2 & w/(x.0,m1)/(x.3,m2).x = w/(
            x.0,m1).x by A54,A47,FUNCT_7:32,128,ZF_LANG1:76;
            then
A71:        L.a1,w/(x.0,m1)/(x.3,m2) |= x.3 'in' x by A65,A70,ZF_MODEL:13;
            w/(x.0,m1) = v/(x,mu)/(x.0,m1) by ZFMODEL2:8;
            then L.a1,w/(x.0,m1)/(x.3,m2) |= p/(x.4,x.0) by A52,A55,A69,
ZFMODEL2:6;
            then L.a1,w/(x.0,m1)/(x.3,m2) |= x.3 'in' x '&' (p/(x.4,x.0)) by
A71,ZF_MODEL:15;
            then L.a1,w/(x.0,m1) |= q by ZF_LANG1:73;
            then u1 in { m where m is Element of L.a1: L.a1,w/(x.0,m) |= q };
            hence thesis by A61,Def1;
          end;
          Section(q,w) c= F.:u
          proof
            let u1;
A72:        L.a1 c= M by ZF_REFLE:16;
            assume u1 in Section(q,w);
            then u1 in { m where m is Element of L.a1: L.a1,w/(x.0,m) |= q }
            by A61,Def1;
            then consider m1 being Element of L.a1 such that
A73:        u1 = m1 and
A74:        L.a1,w/(x.0,m1) |= q;
            consider m2 being Element of L.a1 such that
A75:        L.a1,w/(x.0,m1)/(x.3,m2) |= x.3 'in' x '&' (p/(x.4,x.0))
            by A74,ZF_LANG1:73;
            m1 in L.a1 & m2 in L.a1;
            then reconsider u9 = m1, u2 = m2 as Element of M by A72;
A76:        w/(x.0,m1) = v/(x,mu)/(x.0,m1) by ZFMODEL2:8;
            L.a1,w/(x.0,m1)/(x.3,m2) |= p/(x.4,x.0) by A75,ZF_MODEL:15;
            then L.a1,v/(x.3,m2)/(x.0,m1)/(x,mu) |= p/(x.4,x.0) by A52,A55,A76,
ZFMODEL2:6;
            then
A77:        L.a1,v/(x.3,m2)/(x.0,m1) |= p/(x.4,x.0) by A53,ZFMODEL2:5;
A78:        f/(x.3,u2)/(x.0,u9)/(x.4,u9) = f/(x.3,u2)/(x.4,u9)/(x.0,u9)
            & f/(x.3,u2)/(x. 0,u9).(x.0) = u9 by FUNCT_7:33,128,ZF_LANG1:76;
            f/(x.3,u2)/(x.0,u9) = M!(v/(x.3,m2)/(x.0,m1)) by ZF_LANG1:def 1
,ZF_REFLE:16;
            then M,f/(x.3,u2)/(x.0,u9) |= p/(x.4,x.0) by A36,A37,A38,A77;
            then M,f/(x.3,u2)/(x.4,u9)/(x.0,u9) |= p by A32,A78,ZFMODEL2:12;
            then M,f/(x.3,u2)/(x.4,u9) |= p by A32,ZFMODEL2:5;
            then
A79:        F.u2 = u9 by A11,A22,ZFMODEL2:10;
A80:        w.x = w/(x.0,m1).x & w.x = mu by A51,A47,FUNCT_7:32,128,ZF_LANG1:76
;
A81:        L.a1,w/(x.0,m1)/(x.3,m2) |= x.3 'in' x by A75,ZF_MODEL:15;
A82:        dom F = M by FUNCT_2:def 1;
            w/(x.0,m1)/(x.3,m2).(x.3) = m2 & w/(x.0,m1)/(x.3,m2).x = w/(
            x.0,m1).x by A54,A47,FUNCT_7:32,128,ZF_LANG1:76;
            then m2 in u by A81,A80,ZF_MODEL:13;
            hence thesis by A73,A79,A82,FUNCT_1:def 6;
          end;
          hence thesis by A62,XBOOLE_0:def 10;
        end;
        suppose
A83:      not x.4 in Free H;
          4<>k+5 by NAT_1:11;
          then
A84:      x.(k+5)<>x.4 by ZF_LANG1:76;
A85:      x.(k+10)<>x.0 by A51,A47,ZF_LANG1:76;
          ( not x.(k+5) in variables_in H)& x.(k+5)<>x.0 by A9,A31,ZF_LANG1:76;
          then not x.0 in Free q by A83,A85,A84,Lm4;
          then Section(q,w)={} by Def1;
          hence thesis by A8,A83,Lm3;
        end;
      end;
      hence thesis;
    end;
    L.a1 in M by A4;
    hence def_func'(H,f).:u in M by A5,A57,Def2;
  end;
  Union L is epsilon-transitive
  proof
    let X;
    assume X in Union L;
    then consider u such that
A86: u in dom L and
A87: X in L.u by Lm1;
    reconsider u as Ordinal by A86;
    u in On W by A86,ZF_REFLE:def 2;
    then reconsider u as Ordinal of W by ZF_REFLE:7;
    L.u is epsilon-transitive by A4;
    then
A88: X c= L.u by A87,ORDINAL1:def 2;
    let u1;
A89: L.u c= Union L by ZF_REFLE:16;
    assume u1 in X;
    then u1 in L.u by A88;
    hence thesis by A89;
  end;
  hence thesis by A6,ZFMODEL1:15;
end;

Lm5: x.i in Free H implies {[i,m]} \/ (v*decode)|((code Free H)\{i})=(v/(x.i,m
)*decode)|code Free H
proof
  set e=v/(x.i,m)*decode;
  set f=v*decode;
  set b=f|((code Free H)\{i});
A1: i in {i} by TARSKI:def 1;
A2: dom(e|{i})=(dom e) /\ {i} by RELAT_1:61
    .=omega /\ {i} by ZF_FUND1:31
    .={i} by ZFMISC_1:46;
  then
A3: (e|{i})={[i,(e|{i}).i]} by GRFUNC_1:7
    .={[i,e.i]} by A1,A2,FUNCT_1:47
    .={[i,e.x".x.i]} by ZF_FUND1:def 3
    .={[i,(v/(x.i,m)).x.i]} by ZF_FUND1:32
    .={[i,m]} by FUNCT_7:128;
A4: dom b=(dom f) /\ ((code Free H)\{i}) by RELAT_1:61
    .=omega /\ ((code Free H)\{i}) by ZF_FUND1:31
    .=dom e /\ ((code Free H)\{i}) by ZF_FUND1:31
    .=dom(e|((code Free H)\{i})) by RELAT_1:61;
  now
    let u;
    assume
A5: u in dom b;
    then u in (dom f) /\ ((code Free H)\{i}) by RELAT_1:61;
    then
A6: u in (code Free H) \ {i} by XBOOLE_0:def 4;
    then u in code Free H by XBOOLE_0:def 5;
    then consider x such that
    x in Free H and
A7: u=x".x by ZF_FUND1:33;
    not u in {i} by A6,XBOOLE_0:def 5;
    then i<>x".x by A7,TARSKI:def 1;
    then
A8: x<>x.i by ZF_FUND1:def 3;
    thus b.u = f.u by A5,FUNCT_1:47
      .=v.x by A7,ZF_FUND1:32
      .=(v/(x.i,m)).x by A8,FUNCT_7:32
      .=e.u by A7,ZF_FUND1:32
      .=(e|((code Free H)\{i})).u by A4,A5,FUNCT_1:47;
  end;
  then
A9: b=e|((code Free H)\{i}) by A4,FUNCT_1:2;
  assume x.i in Free H;
  then x".x.i in code Free H by ZF_FUND1:33;
  then i in code Free H by ZF_FUND1:def 3;
  then {i} c= code Free H by ZFMISC_1:31;
  then e|code Free H=(e|({i} \/ ((code Free H)\{i}))) by XBOOLE_1:45
    .={[i,m]} \/ b by A3,A9,RELAT_1:78;
  hence thesis;
end;

theorem Th4:
  Section(H,v)= {m : {[{},m]} \/ (v*decode)|((code Free H)\{{}}) in
  Diagram(H,M)}
proof
  set S=Section(H,v);
  set D={m:{[{},m]}\/(v*decode)|((code Free H)\{{}}) in Diagram(H,M)};
  now
    per cases;
    suppose
A1:   x.0 in Free H;
      then
A2:   S={m: M,v/(x.0,m) |= H} by Def1;
A3:   D c= S
      proof
        let u;
        assume u in D;
        then consider m such that
A4:     m=u and
A5:     {[{},m]}\/(v*decode)|((code Free H)\{{}}) in Diagram(H,M);
        (v/(x.0,m)*decode)|code Free H in Diagram(H,M) by A1,A5,Lm5;
        then
        ex v1 st (v/(x.0,m)*decode)|code Free H=(v1*decode)|code Free H &
        v1 in St(H,M) by ZF_FUND1:def 5;
        then v/(x.0,m) in St(H,M) by ZF_FUND1:36;
        then M,v/(x.0,m) |= H by ZF_MODEL:def 4;
        hence thesis by A2,A4;
      end;
      S c= D
      proof
        let u;
        assume u in S;
        then consider m such that
A6:     m=u and
A7:     M,v/(x.0,m) |= H by A2;
        v/(x.0,m) in St(H,M) by A7,ZF_MODEL:def 4;
        then (v/(x.0,m)*decode)|code Free H in Diagram(H,M) by ZF_FUND1:def 5;
        then {[{},m]}\/(v*decode)|((code Free H)\{{}}) in Diagram(H,M) by A1
,Lm5;
        hence thesis by A6;
      end;
      hence thesis by A3,XBOOLE_0:def 10;
    end;
    suppose
A8:   not x.0 in Free H;
      now
        set u = the Element of D;
        assume D<>{};
        then u in D;
        then consider m such that
        m=u and
A9:     {[{},m]}\/(v*decode)|((code Free H)\{{}}) in Diagram(H,M);
        consider v2 such that
A10:    ({[{},m]}\/(v*decode)|((code Free H)\{{}})) =(v2*decode)|code
        Free H and
        v2 in St(H,M) by A9,ZF_FUND1:def 5;
        reconsider w={[{},m]}\/(v*decode)|((code Free H)\{{}}) as Function by
A10;
        [{},m]in{[{},m]} by TARSKI:def 1;
        then [{},m] in w by XBOOLE_0:def 3;
        then {} in dom w by FUNCT_1:1;
        then {} in dom(v2*decode)/\(code Free H) by A10,RELAT_1:61;
        then {} in code Free H by XBOOLE_0:def 4;
        then ex y st y in Free H & {}=x".y by ZF_FUND1:33;
        hence contradiction by A8,ZF_FUND1:def 3;
      end;
      hence thesis by A8,Def1;
    end;
  end;
  hence thesis;
end;

theorem Th5:
  Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is
  predicatively_closed
proof
  assume that
A1: Y is closed_wrt_A1-A7 and
A2: Y is epsilon-transitive;
  let H,E,f such that
A3: E in Y;
  now
    per cases;
    suppose
      not x.0 in Free H;
      then Section(H,f)={} by Def1;
      hence thesis by A1,ZF_FUND1:3;
    end;
    suppose
A4:   x.0 in Free H;
      reconsider a=E as Element of W by A3;
      reconsider n={} as Element of omega by ORDINAL1:def 11;
      set fs=(code Free H)\{n};
A5:   Diagram(H,E) in Y by A1,A3,ZF_FUND1:22;
      then reconsider b=Diagram(H,E) as Element of W;
A6:   b c= Funcs(fs \/ {n},a)
      proof
        let u;
        assume u in b;
        then ex f1 st u=(f1*decode)|code Free H & f1 in St(H,E) by
ZF_FUND1:def 5;
        then
A7:     u in Funcs(code Free H,a) by ZF_FUND1:31;
        x".x.0 in code Free H by A4,ZF_FUND1:33;
        then n in code Free H by ZF_FUND1:def 3;
        then {n} c= code Free H by ZFMISC_1:31;
        hence thesis by A7,XBOOLE_1:45;
      end;
      n in {n} by TARSKI:def 1;
      then
A8:   not n in fs by XBOOLE_0:def 5;
A9:   (f*decode)|fs in Funcs(fs,a) by ZF_FUND1:31;
      Funcs(fs,a) in Y by A1,A3,ZF_FUND1:9;
      then reconsider y=(f*decode)|fs as Element of W by A9,ZF_FUND1:1;
      set B={e: {[n,e]} \/ y in b};
      set A={w: w in a & {[n,w]} \/ y in b};
A10:  A=B
      proof
        thus A c= B
        proof
          let u;
          assume u in A;
          then ex w st u=w & w in a & {[n,w]} \/ y in b;
          hence thesis;
        end;
        let u;
        assume u in B;
        then consider e such that
A11:    u=e and
A12:    {[n,e]} \/ y in b;
        reconsider e as Element of W by A3,ZF_FUND1:1;
        e in A by A12;
        hence thesis by A11;
      end;
      a c= Y by A2,A3,ORDINAL1:def 2;
      then A in Y by A1,A3,A5,A9,A8,A6,ZF_FUND1:16;
      hence thesis by A10,Th4;
    end;
  end;
  hence thesis;
end;

theorem
  omega in W & (for a,b st a in b holds L.a c= L.b) & (for a st a <> {}
& a is limit_ordinal holds L.a = Union (L|a)) & (for a holds L.a in Union L & L
  .a is epsilon-transitive) & Union L is closed_wrt_A1-A7 implies Union L is
  being_a_model_of_ZF
proof
  assume that
A1: omega in W and
A2: for a,b st a in b holds L.a c= L.b and
A3: for a st a <> {} & a is limit_ordinal holds L.a = Union (L|a) and
A4: for a holds L.a in Union L & L.a is epsilon-transitive and
A5: Union L is closed_wrt_A1-A7;
A6: Union L is epsilon-transitive
  proof
    let X;
    assume X in Union L;
    then consider u such that
A7: u in dom L and
A8: X in L.u by Lm1;
    reconsider u as Ordinal by A7;
    u in On W by A7,ZF_REFLE:def 2;
    then reconsider u as Ordinal of W by ZF_REFLE:7;
    L.u is epsilon-transitive by A4;
    then
A9: X c= L.u by A8,ORDINAL1:def 2;
    let u1;
A10: L.u c= Union L by ZF_REFLE:16;
    assume u1 in X;
    then u1 in L.u by A9;
    hence thesis by A10;
  end;
  then Union L is predicatively_closed by A5,Th5;
  then
A11: Union L |= the_axiom_of_power_sets & for H st {x.0,x.1,x.2} misses
  Free H holds Union L |= the_axiom_of_substitution_for H by A1,A2,A3,A4,Th2
,Th3;
  for u st u in Union L holds union u in Union L by A5,ZF_FUND1:2;
  then
A12: Union L |= the_axiom_of_unions by A6,ZFMODEL1:5;
  for u1,u2 st u1 in Union L & u2 in Union L holds {u1,u2} in Union L by A5,
ZF_FUND1:6;
  then
A13: Union L |= the_axiom_of_pairs by A6,ZFMODEL1:3;
  ex u st u in Union L & u<>{} & for u1 st u1 in u ex u2 st u1 c< u2 & u2 in u
  proof
A14: card omega in card W by A1,CLASSES2:1;
    deffunc G(set,set) = inf {w: L.$2 in L.w};
    consider ksi being Function such that
A15: dom ksi=NAT & ksi.0=0-element_of(W) & for i being Nat holds ksi.(
    i+1)=G(i,ksi.i) from NAT_1:sch 11;
    card rng ksi c= card NAT by A15,CARD_1:12;
    then
A16: card rng ksi in card W by A14,ORDINAL1:12;
    set lambda=sup rng ksi;
A17: for i holds ksi.i in On W & ksi.i is Ordinal of W
    proof
      defpred P[Element of NAT] means ksi.$1 in On W & ksi.$1 is Ordinal of W;
A18:  now
        let i;
        assume P[i];
        then reconsider a=ksi.i as Ordinal of W;
A19:    ksi.(i+1)=inf {w: L.a in L.w} by A15;
        consider u such that
A20:    u in dom L and
A21:    L.a in L.u by A4,Lm1;
        dom L=On W by ZF_REFLE:def 2;
        then reconsider b=u as Ordinal of W by A20,ZF_REFLE:7;
        b in {w: L.a in L.w} by A21;
        then inf {w: L.a in L.w} c= b by ORDINAL2:14;
        then ksi.(i+1) in W by A19,CLASSES1:def 1;
        hence P[i+1] by A19,ORDINAL1:def 9;
      end;
A22:  P[0] by A15,ZF_REFLE:7;
      thus P[i] from NAT_1:sch 1(A22,A18);
    end;
    rng ksi c= W
    proof
      let a be set;
      assume a in rng ksi;
      then consider i being set such that
A23:  i in dom ksi and
A24:  a=ksi.i by FUNCT_1:def 3;
      reconsider i as Element of NAT by A15,A23;
      ksi.i in On W by A17;
      hence thesis by A24,ORDINAL1:def 9;
    end;
    then rng ksi in W by A16,CLASSES1:1;
    then reconsider l=lambda as Ordinal of W by ZF_REFLE:19;
A25: for i holds L.(ksi.i) in L.(ksi.(i+1))
    proof
      let i;
      reconsider a=ksi.i as Ordinal of W by A17;
      consider b being set such that
A26:  b in dom L and
A27:  L.a in L.b by A4,Lm1;
      b in On W by A26,ZF_REFLE:def 2;
      then reconsider b as Ordinal of W by ZF_REFLE:7;
A28:  b in {w: L.a in L.w} by A27;
      ksi.(i+1)=inf {w: L.(ksi.i) in L.w} by A15;
      then ksi.(i+1) in {w: L.(ksi.i) in L.w} by A28,ORDINAL2:17;
      then ex w st w=ksi.(i+1) & L.a in L.w;
      hence thesis;
    end;
A29: for i holds ksi.i in ksi.(i+1)
    proof
      let i;
      reconsider b=ksi.(i+1) as Ordinal of W by A17;
      reconsider a=ksi.i as Ordinal of W by A17;
      assume not ksi.i in ksi.(i+1);
      then b=a or b in a by ORDINAL1:14;
      then L.b c= L.a by A2;
      hence contradiction by A25,ORDINAL1:5;
    end;
A30: l c= union l
    proof
      let u1 be Ordinal;
      assume u1 in l;
      then consider u2 being Ordinal such that
A31:  u2 in rng ksi and
A32:  u1 c= u2 by ORDINAL2:21;
      consider i being set such that
A33:  i in dom ksi and
A34:  u2=ksi.i by A31,FUNCT_1:def 3;
      reconsider i as Element of NAT by A15,A33;
      reconsider u3=ksi.(i+1) as Ordinal of W by A17;
      u3 in rng ksi by A15,FUNCT_1:def 3;
      then
A35:  u3 in l by ORDINAL2:19;
      u1 in u3 by A29,A32,A34,ORDINAL1:12;
      hence thesis by A35,TARSKI:def 4;
    end;
    union l c= l by ORDINAL2:5;
    then l=union l by A30,XBOOLE_0:def 10;
    then
A36: l is limit_ordinal by ORDINAL1:def 6;
A37: union {L.(ksi.n): not contradiction}=L.l
    proof
      set A={L.(ksi.n): not contradiction};
      thus union A c= L.l
      proof
        let u1;
        assume u1 in union A;
        then consider X such that
A38:    u1 in X and
A39:    X in A by TARSKI:def 4;
        consider n such that
A40:    X=L.(ksi.n) by A39;
        reconsider a=ksi.n as Ordinal of W by A17;
        a in rng ksi by A15,FUNCT_1:def 3;
        then L.a c= L.l by A2,ORDINAL2:19;
        hence thesis by A38,A40;
      end;
      0-element_of W in rng ksi by A15,FUNCT_1:def 3;
      then l<>{} by ORDINAL2:19;
      then
A41:  L.l=Union(L|l) by A3,A36;
      let u1;
      assume u1 in L.l;
      then consider u2 such that
A42:  u2 in dom(L|l) and
A43:  u1 in (L|l).u2 by A41,Lm1;
A44:  u1 in L.u2 by A42,A43,FUNCT_1:47;
A45:  u2 in (dom L) /\ l by A42,RELAT_1:61;
      then
A46:  u2 in l by XBOOLE_0:def 4;
      u2 in dom L by A45,XBOOLE_0:def 4;
      then u2 in On W by ZF_REFLE:def 2;
      then reconsider u2 as Ordinal of W by ZF_REFLE:7;
      consider b being Ordinal such that
A47:  b in rng ksi and
A48:  u2 c= b by A46,ORDINAL2:21;
      consider i being set such that
A49:  i in dom ksi and
A50:  b=ksi.i by A47,FUNCT_1:def 3;
      reconsider i as Element of NAT by A15,A49;
      b=ksi.i by A50;
      then reconsider b as Ordinal of W by A17;
      u2 c< b iff u2 c= b & u2 <> b by XBOOLE_0:def 8;
      then
A51:  L.u2 c= L.b by A2,A48,ORDINAL1:11;
      L.(ksi.i) in A;
      hence thesis by A44,A50,A51,TARSKI:def 4;
    end;
    take u = L.lambda;
    L.l in Union L by A4;
    hence u in Union L & u<>{};
    let u1;
    assume u1 in u;
    then consider u2 such that
A52: u1 in u2 & u2 in {L.(ksi.n): not contradiction} by A37,TARSKI:def 4;
    take u2;
    consider i such that
A53: u2=L.(ksi.i) by A52;
A54: u1<>u2 by A52;
    reconsider a=ksi.i as Ordinal of W by A17;
    L.a is epsilon-transitive by A4;
    then u1 c= u2 by A52,A53,ORDINAL1:def 2;
    hence u1 c< u2 by A54,XBOOLE_0:def 8;
A55: L.(ksi.(i+1)) in {L.(ksi.n): not contradiction};
    L.(ksi.i) in L.(ksi.(i+1)) by A25;
    hence u2 in u by A37,A53,A55,TARSKI:def 4;
  end;
  then Union L |= the_axiom_of_infinity by A6,ZFMODEL1:7;
  hence thesis by A6,A13,A12,A11,ZF_MODEL:def 12;
end;