:: A Model of ZF Set Theory Language
::  by Grzegorz Bancerek
::
:: Received April 4, 1989
:: Copyright (c) 1990-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, SUBSET_1, XBOOLE_0, FINSEQ_1, XXREAL_0, TARSKI, ARYTM_3,
      CARD_1, ORDINAL4, FUNCT_1, XBOOLEAN, BVFUNC_2, RELAT_1, CLASSES2, NAT_1,
      ARYTM_1, ZF_LANG;
 notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ORDINAL1,
      NAT_1, NUMBERS, FINSEQ_1, XXREAL_0;
 constructors XXREAL_0, XREAL_0, NAT_1, FINSEQ_1;
 registrations SUBSET_1, ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, CARD_1,
      XBOOLE_0;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 definitions TARSKI;
 theorems TARSKI, FUNCT_1, NAT_1, FINSEQ_1, XBOOLE_0, XREAL_1, XXREAL_0,
      ORDINAL1;
 schemes NAT_1, XBOOLE_0;

begin

reserve k,m,n for Element of NAT,
  a,X,Y for set,
  D,D1,D2 for non empty set;
reserve p,q for FinSequence of NAT;

::
::       The Construction of ZF Set Theory Language
::
:: The set and the mode of ZF-language variables

definition
  func VAR -> Subset of NAT equals
  { k : 5 <= k };
  coherence
  proof
    set X = { k : 5 <= k };
    X c= NAT
    proof
      let a;
      assume a in X;
      then ex k st a = k & 5 <= k;
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  cluster VAR -> non empty;
  coherence
  proof
    5 in { k : 5 <= k };
    hence thesis;
  end;
end;

definition
  mode Variable is Element of VAR;
end;

definition
  let n;
  func x.n -> Variable equals
  5 + n;
  coherence
  proof
    set x = 5 + n;
    5 <= x by NAT_1:11;
    then x in { k : 5 <= k };
    hence thesis;
  end;
end;

reserve x,y,z,t for Variable;

:: The operations to make ZF-formulae

definition
  let x;
  redefine func <*x*> -> FinSequence of NAT;
  coherence
  proof
    reconsider VAR9 = VAR as non empty Subset of NAT;
    reconsider x9 = x as Element of VAR9;
    reconsider x9 as Element of NAT;
    <*x9*> is FinSequence of NAT;
    hence thesis;
  end;
end;

definition
  let x,y;
  func x '=' y -> FinSequence of NAT equals
  <*0*>^<*x*>^<*y*>;
  coherence;
  func x 'in' y -> FinSequence of NAT equals
  <*1*>^<*x*>^<*y*>;
  coherence;
end;

theorem
  x '=' y = z '=' t implies x = z & y = t
proof
A1: <*0*>^<*x*>^<*y*> = <*0*>^(<*x*>^<*y*>) & <*0*>^<*z*>^<*t*> = <*0*>^(<*z
  *>^ <*t*>) by FINSEQ_1:32;
A2: <*x,y*>.1 = x & <*x,y*>.2 = y by FINSEQ_1:44;
A3: <*x*>^<*y*> = <*x,y*> & <*z*>^<*t*> = <*z,t*> by FINSEQ_1:def 9;
A4: <*z,t*>.1 = z & <*z,t*>.2 = t by FINSEQ_1:44;
  assume x '=' y = z '=' t;
  hence thesis by A1,A2,A4,A3,FINSEQ_1:33;
end;

theorem
  x 'in' y = z 'in' t implies x = z & y = t
proof
A1: <*1*>^<*x*>^<*y*> = <*1*>^(<*x*>^<*y*>) & <*1*>^<*z*>^<*t*> = <*1*>^(<*z
  *>^ <*t*>) by FINSEQ_1:32;
A2: <*x,y*>.1 = x & <*x,y*>.2 = y by FINSEQ_1:44;
A3: <*x*>^<*y*> = <*x,y*> & <*z*>^<*t*> = <*z,t*> by FINSEQ_1:def 9;
A4: <*z,t*>.1 = z & <*z,t*>.2 = t by FINSEQ_1:44;
  assume x 'in' y = z 'in' t;
  hence thesis by A1,A2,A4,A3,FINSEQ_1:33;
end;

definition
  let p;
  func 'not' p -> FinSequence of NAT equals
  <*2*>^p;
  coherence;
  let q;
  func p '&' q -> FinSequence of NAT equals
  <*3*>^p^q;
  coherence;
end;

definition
  let x,p;
  func All(x,p)-> FinSequence of NAT equals
  <*4*>^<*x*>^p;
  coherence;
end;

theorem Th3:
  All(x,p) = All(y,q) implies x = y & p = q
proof
A1: <*4*>^<*x*>^p = <*4*>^(<*x*>^p) & <*4*>^<*y*>^q = <*4*>^(<*y*>^q) by
FINSEQ_1:32;
A2: (<*x*>^p).1 = x & (<*y*>^q).1 = y by FINSEQ_1:41;
  assume
A3: All(x,p) = All(y,q);
  hence x = y by A1,A2,FINSEQ_1:33;
  <*x*>^p = <*y*>^q by A3,A1,FINSEQ_1:33;
  hence thesis by A2,FINSEQ_1:33;
end;

:: The set of all well formed formulae of ZF-language

definition
  func WFF -> non empty set means
  :Def8:
  (for a st a in it holds a is
FinSequence of NAT ) & (for x,y holds x '=' y in it & x 'in' y in it ) & (for p
st p in it holds 'not' p in it ) & (for p,q st p in it & q in it holds p '&' q
in it ) & (for x,p st p in it holds All(x,p) in it ) & for D st (for a st a in
D holds a is FinSequence of NAT ) & (for x,y holds x '=' y in D & x 'in' y in D
) & (for p st p in D holds 'not' p in D ) & (for p,q st p in D & q in D holds p
  '&' q in D ) & (for x,p st p in D holds All(x,p) in D ) holds it c= D;
  existence
  proof
    defpred P[set] means (for a st a in $1 holds a is FinSequence of NAT ) & (
for x,y holds x '=' y in $1 & x 'in' y in $1 ) & (for p st p in $1 holds 'not'
p in $1 ) & (for p,q st p in $1 & q in $1 holds p '&' q in $1 ) & (for x,p st p
    in $1 holds All(x,p) in $1 );
    defpred Y[set] means for D st P[D] holds $1 in D;
    consider Y such that
A1: a in Y iff a in NAT* & Y[a] from XBOOLE_0:sch 1;
    now
      set a = x.0 '=' x.0;
      take b = a;
      a in NAT* & for D st P[D] holds a in D by FINSEQ_1:def 11;
      hence b in Y by A1;
    end;
    then reconsider Y as non empty set;
    take Y;
    thus a in Y implies a is FinSequence of NAT
    proof
      assume a in Y;
      then a in NAT* by A1;
      hence thesis by FINSEQ_1:def 11;
    end;
    thus x '=' y in Y & x 'in' y in Y
    proof
      x '=' y in NAT* & for D st P[D] holds x '=' y in D by FINSEQ_1:def 11;
      hence x '=' y in Y by A1;
      x 'in' y in NAT* & for D st P[D] holds x 'in' y in D by FINSEQ_1:def 11;
      hence thesis by A1;
    end;
    thus p in Y implies 'not' p in Y
    proof
      assume
A2:   p in Y;
A3:   for D st P[D] holds 'not' p in D
      proof
        let D;
        assume
A4:     P[D];
        then p in D by A1,A2;
        hence thesis by A4;
      end;
      'not' p in NAT* by FINSEQ_1:def 11;
      hence thesis by A1,A3;
    end;
    thus q in Y & p in Y implies q '&' p in Y
    proof
      assume
A5:   q in Y & p in Y;
A6:   for D st P[D] holds q '&' p in D
      proof
        let D;
        assume
A7:     P[D];
        then p in D & q in D by A1,A5;
        hence thesis by A7;
      end;
      q '&' p in NAT* by FINSEQ_1:def 11;
      hence thesis by A1,A6;
    end;
    thus for x,p st p in Y holds All(x,p) in Y
    proof
      let x,p such that
A8:   p in Y;
A9:   for D st P[D] holds All(x,p) in D
      proof
        let D;
        assume
A10:    P[D];
        then p in D by A1,A8;
        hence thesis by A10;
      end;
      All(x,p) in NAT* by FINSEQ_1:def 11;
      hence thesis by A1,A9;
    end;
    let D such that
A11: P[D];
    let a;
    assume a in Y;
    hence thesis by A1,A11;
  end;
  uniqueness
  proof
    let D1,D2;
    assume ( ( for a st a in D1 holds a is FinSequence of NAT)& for x,y
holds x '=' y in D1 & x 'in' y in D1 )&( ( for p st p in D1 holds 'not' p in D1
)& for p,q st p in D1 & q in D1 holds p '&' q in D1 ) & ( for x,p st p in D1
holds All(x,p) in D1)&( ( for D st (for a st a in D holds a is FinSequence of
    NAT ) & (for x, y holds x '=' y in D & x 'in' y in D ) & ( for p st p in D
holds 'not' p in D ) & (for p,q st p in D & q in D holds p '&' q in D ) & (for
x,p st p in D holds All (x,p) in D ) holds D1 c= D)& for a st a in D2 holds a
is FinSequence of NAT ) &( ( ( for x,y holds x '=' y in D2 & x 'in' y in D2)&
for p st p in D2 holds 'not' p in D2 )&( ( for p,q st p in D2 & q in D2 holds p
'&' q in D2)& for x,p st p in D2 holds All(x,p) in D2 ) & for D st (for a st a
in D holds a is FinSequence of NAT ) & (for x, y holds x '=' y in D & x 'in' y
in D ) & (for p st p in D holds 'not' p in D ) & (for p,q st p in D & q in D
holds p '&' q in D ) & (for x,p st p in D holds All(x,p) in D ) holds D2 c= D )
    ;
    then D1 c= D2 & D2 c= D1;
    hence thesis by XBOOLE_0:def 10;
  end;
end;

definition
  let IT be FinSequence of NAT;
  attr IT is ZF-formula-like means
  :Def9:
  IT is Element of WFF;
end;

registration
  cluster ZF-formula-like for FinSequence of NAT;
  existence
  proof
    set x = the Element of WFF;
    reconsider x as FinSequence of NAT by Def8;
    take x;
    thus x is Element of WFF;
  end;
end;

definition
  mode ZF-formula is ZF-formula-like FinSequence of NAT;
end;

theorem
  a is ZF-formula iff a in WFF
proof
  thus a is ZF-formula implies a in WFF
  proof
    assume a is ZF-formula;
    then a is Element of WFF by Def9;
    hence thesis;
  end;
  assume a in WFF;
  hence thesis by Def8,Def9;
end;

reserve F,F1,G,G1,H,H1 for ZF-formula;

registration
  let x,y;
  cluster x '=' y -> ZF-formula-like;
  coherence
  proof
    x '=' y is Element of WFF by Def8;
    hence thesis by Def9;
  end;
  cluster x 'in' y -> ZF-formula-like;
  coherence
  proof
    x 'in' y is Element of WFF by Def8;
    hence thesis by Def9;
  end;
end;

registration
  let H;
  cluster 'not' H -> ZF-formula-like;
  coherence
  proof
    H is Element of WFF by Def9;
    then 'not' H is Element of WFF by Def8;
    hence thesis by Def9;
  end;
  let G;
  cluster H '&' G -> ZF-formula-like;
  coherence
  proof
    H is Element of WFF & G is Element of WFF by Def9;
    then H '&' G is Element of WFF by Def8;
    hence thesis by Def9;
  end;
end;

registration
  let x,H;
  cluster All(x,H) -> ZF-formula-like;
  coherence
  proof
    H is Element of WFF by Def9;
    then All(x,H) is Element of WFF by Def8;
    hence thesis by Def9;
  end;
end;

::
::                   The Properties of ZF-formulae
::

definition
  let H;
  attr H is being_equality means
  :Def10:
  ex x,y st H = x '=' y;
  attr H is being_membership means
  :Def11:
  ex x,y st H = x 'in' y;
  attr H is negative means
  :Def12:
  ex H1 st H = 'not' H1;
  attr H is conjunctive means
  :Def13:
  ex F,G st H = F '&' G;
  attr H is universal means
  :Def14:
  ex x,H1 st H = All(x,H1);
end;

theorem
  (H is being_equality iff ex x,y st H = x '=' y) & (H is
being_membership iff ex x,y st H = x 'in' y) & (H is negative iff ex H1 st H =
'not' H1) & (H is conjunctive iff ex F,G st H = F '&' G) & (H is universal iff
  ex x,H1 st H = All(x,H1) ) by Def10,Def11,Def12,Def13,Def14;

definition
  let H;
  attr H is atomic means
  :Def15:
  H is being_equality or H is being_membership;
end;

definition
  let F,G;
  func F 'or' G -> ZF-formula equals
  'not'('not' F '&' 'not' G);
  coherence;
  func F => G -> ZF-formula equals
  'not' (F '&' 'not' G);
  coherence;
end;

definition
  let F,G;
  func F <=> G -> ZF-formula equals
  (F => G) '&' (G => F);
  coherence;
end;

definition
  let x,H;
  func Ex(x,H) -> ZF-formula equals
  'not' All(x,'not' H);
  coherence;
end;

definition
  let H;
  attr H is disjunctive means
  :Def20:
  ex F,G st H = F 'or' G;
  attr H is conditional means
  :Def21:
  ex F,G st H = F => G;
  attr H is biconditional means
  :Def22:
  ex F,G st H = F <=> G;
  attr H is existential means
  :Def23:
  ex x,H1 st H = Ex(x,H1);
end;

theorem
  (H is disjunctive iff ex F,G st H = F 'or' G) & (H is conditional iff
ex F,G st H = F => G) & (H is biconditional iff ex F,G st H = F <=> G) & (H is
  existential iff ex x,H1 st H = Ex(x,H1) ) by Def20,Def21,Def22,Def23;

definition
  let x,y,H;
  func All(x,y,H) -> ZF-formula equals
  All(x,All(y,H));
  coherence;
  func Ex(x,y,H) -> ZF-formula equals
  Ex(x,Ex(y,H));
  coherence;
end;

theorem
  All(x,y,H) = All(x,All(y,H)) & Ex(x,y,H) = Ex(x,Ex(y,H));

definition
  let x,y,z,H;
  func All(x,y,z,H) -> ZF-formula equals
  All(x,All(y,z,H));
  coherence;
  func Ex(x,y,z,H) -> ZF-formula equals
  Ex(x,Ex(y,z,H));
  coherence;
end;

theorem
  All(x,y,z,H) = All(x,All(y,z,H)) & Ex(x,y,z,H) = Ex(x,Ex(y,z,H));

theorem Th9:
  H is being_equality or H is being_membership or H is negative or
  H is conjunctive or H is universal
proof
A1: H is Element of WFF by Def9;
  assume
A2: not thesis;
  then x.0 '=' x.1 <> H by Def10;
  then
A3: not x.0 '=' x.1 in { H } by TARSKI:def 1;
A4: now
    let x,y;
    x '=' y <> H by A2,Def10;
    then
A5: not x '=' y in { H } by TARSKI:def 1;
    x '=' y in WFF by Def8;
    hence x '=' y in WFF \ { H } by A5,XBOOLE_0:def 5;
    x 'in' y <> H by A2,Def11;
    then
A6: not x 'in' y in { H } by TARSKI:def 1;
    x 'in' y in WFF by Def8;
    hence x 'in' y in WFF \ { H } by A6,XBOOLE_0:def 5;
  end;
A7: now
    let x,p;
    assume
A8: p in WFF \ { H };
    then reconsider H1 = p as ZF-formula by Def9;
    All(x,H1) <> H by A2,Def14;
    then
A9: not All(x,p) in { H } by TARSKI:def 1;
    All(x,p) in WFF by A8,Def8;
    hence All(x,p) in WFF \ { H } by A9,XBOOLE_0:def 5;
  end;
A10: now
    let p,q;
    assume
A11: p in WFF \ { H } & q in WFF \ { H };
    then reconsider F = p, G = q as ZF-formula by Def9;
    F '&' G <> H by A2,Def13;
    then
A12: not p '&' q in { H } by TARSKI:def 1;
    p '&' q in WFF by A11,Def8;
    hence p '&' q in WFF \ { H } by A12,XBOOLE_0:def 5;
  end;
A13: now
    let p;
    assume
A14: p in WFF \ { H };
    then reconsider H1 = p as ZF-formula by Def9;
    'not' H1 <> H by A2,Def12;
    then
A15: not 'not' p in { H } by TARSKI:def 1;
    'not' p in WFF by A14,Def8;
    hence 'not' p in WFF \ { H } by A15,XBOOLE_0:def 5;
  end;
  x.0 '=' x.1 in WFF by Def8;
  then
A16: WFF \ { H } is non empty set by A3,XBOOLE_0:def 5;
  for a st a in WFF \ { H } holds a is FinSequence of NAT by Def8;
  then WFF c= WFF \ { H } by A16,A4,A13,A10,A7,Def8;
  then H in WFF \ { H } by A1,TARSKI:def 3;
  then not H in { H } by XBOOLE_0:def 5;
  hence contradiction by TARSKI:def 1;
end;

theorem Th10:
  H is atomic or H is negative or H is conjunctive or H is universal
proof
  assume ( not H is being_equality)& not H is being_membership;
  hence thesis by Th9;
end;

theorem Th11:
  H is atomic implies len H = 3
proof
A1: now
    assume H is being_equality;
    then consider x,y such that
A2: H = x '=' y by Def10;
    H = <* 0,x,y *> by A2,FINSEQ_1:def 10;
    hence thesis by FINSEQ_1:45;
  end;
A3: now
    assume H is being_membership;
    then consider x,y such that
A4: H = x 'in' y by Def11;
    H = <* 1,x,y *> by A4,FINSEQ_1:def 10;
    hence thesis by FINSEQ_1:45;
  end;
  assume H is atomic;
  hence thesis by A1,A3,Def15;
end;

theorem Th12:
  H is atomic or ex H1 st len H1 + 1 <= len H
proof
A1: now
    let H;
    assume H is universal;
    then consider x,H1 such that
A2: H = All(x,H1) by Def14;
    take H1;
A3: len <*4,x*> = 2 & <*4*>^<*x*> =<*4,x*> by FINSEQ_1:44,def 9;
A4: 1 + 1 + len H1 = 1 + (1 + len H1);
    len H = len(<*4*>^<*x*>) + len H1 by A2,FINSEQ_1:22;
    hence len H1 + 1 <= len H by A3,A4,NAT_1:11;
  end;
A5: now
    let H;
    assume H is negative;
    then consider H1 such that
A6: H = 'not' H1 by Def12;
    take H1;
    len H = len <*2*> + len H1 by A6,FINSEQ_1:22;
    hence len H1 + 1 <= len H by FINSEQ_1:40;
  end;
A7: now
    let H;
    assume H is conjunctive;
    then consider H1,F1 such that
A8: H = H1 '&' F1 by Def13;
    take H1;
A9: len(<*3*>^H1) = len <*3*> + len H1 & len <*3*> = 1 by FINSEQ_1:22,40;
    len H = len(<*3*>^H1) + len F1 by A8,FINSEQ_1:22;
    hence len H1 + 1 <= len H by A9,NAT_1:11;
  end;
  assume not H is atomic;
  then H is negative or H is conjunctive or H is universal by Th10;
  hence thesis by A5,A7,A1;
end;

theorem Th13:
  3 <= len H
proof
  now
    assume not H is atomic;
    then consider H1 such that
A1: len H1 + 1 <= len H by Th12;
A2: now
      assume not H1 is atomic;
      then consider F such that
A3:   len F + 1 <= len H1 by Th12;
A4:   now
        assume not F is atomic;
        then consider F1 such that
A5:     len F1 + 1 <= len F by Th12;
        0 <= len F1 by NAT_1:2;
        then 0 + 1 <= len F1 + 1 by XREAL_1:7;
        then 1 <= len F by A5,XXREAL_0:2;
        then 1 + 1 <= len F + 1 by XREAL_1:7;
        then 2 <= len H1 by A3,XXREAL_0:2;
        then 2 + 1 <= len H1 + 1 by XREAL_1:7;
        hence thesis by A1,XXREAL_0:2;
      end;
A6:   len F + 1 + 1 <= len H1 + 1 by A3,XREAL_1:7;
      now
        assume F is atomic;
        then len F = 3 by Th11;
        then 3 + 1 + 1 <= len H by A1,A6,XXREAL_0:2;
        hence thesis by XXREAL_0:2;
      end;
      hence thesis by A4;
    end;
    now
      assume H1 is atomic;
      then 3 + 1 <= len H by A1,Th11;
      hence thesis by XXREAL_0:2;
    end;
    hence thesis by A2;
  end;
  hence thesis by Th11;
end;

theorem
  len H = 3 implies H is atomic
proof
  assume
A1: len H = 3;
  assume not H is atomic;
  then consider H1 such that
A2: len H1 + 1 <= len H by Th12;
  3 <= len H1 by Th13;
  then 3 + 1 <= len H1 + 1 by XREAL_1:7;
  hence contradiction by A1,A2,XXREAL_0:2;
end;

theorem Th15:
  for x,y holds (x '=' y).1 = 0 & (x 'in' y ).1 = 1
proof
  let x,y;
  thus (x '=' y).1 = (<*0*>^(<*x*>^<*y*>)).1 by FINSEQ_1:32
    .= 0 by FINSEQ_1:41;
  thus (x 'in' y).1 = (<*1*>^(<*x*>^<*y*>)).1 by FINSEQ_1:32
    .= 1 by FINSEQ_1:41;
end;

theorem Th16:
  for F,G holds (F '&' G).1 = 3
proof
  let F,G;
  thus (F '&' G).1 = (<*3*>^(F^G)).1 by FINSEQ_1:32
    .= 3 by FINSEQ_1:41;
end;

theorem Th17:
  for x,H holds All(x,H).1 = 4
proof
  let x,H;
  thus All(x,H).1 = (<*4*>^(<*x*>^H)).1 by FINSEQ_1:32
    .= 4 by FINSEQ_1:41;
end;

theorem Th18:
  H is being_equality implies H.1 = 0
proof
  assume H is being_equality;
  then consider x,y such that
A1: H = x '=' y by Def10;
  H = <* 0,x,y *> by A1,FINSEQ_1:def 10;
  hence thesis by FINSEQ_1:45;
end;

theorem Th19:
  H is being_membership implies H.1 = 1
proof
  assume H is being_membership;
  then consider x,y such that
A1: H = x 'in' y by Def11;
  H = <* 1,x,y *> by A1,FINSEQ_1:def 10;
  hence thesis by FINSEQ_1:45;
end;

theorem Th20:
  H is negative implies H.1 = 2
proof
  assume H is negative;
  then ex H1 st H = 'not' H1 by Def12;
  hence thesis by FINSEQ_1:41;
end;

theorem Th21:
  H is conjunctive implies H.1 = 3
proof
  assume H is conjunctive;
  then consider F,G such that
A1: H = F '&' G by Def13;
  <*3*>^F^G = <*3*>^(F^G) by FINSEQ_1:32;
  hence thesis by A1,FINSEQ_1:41;
end;

theorem Th22:
  H is universal implies H.1 = 4
proof
  assume H is universal;
  then consider x,H1 such that
A1: H = All(x,H1) by Def14;
  <*4*>^<*x*>^H1 = <*4*>^(<*x*>^H1) by FINSEQ_1:32;
  hence thesis by A1,FINSEQ_1:41;
end;

theorem Th23:
  H is being_equality & H.1 = 0 or H is being_membership & H.1 = 1
or H is negative & H.1 = 2 or H is conjunctive & H.1 = 3 or H is universal & H.
  1 = 4
proof
  per cases by Th9;
  case
    H is being_equality;
    hence thesis by Th18;
  end;
  case
    H is being_membership;
    hence thesis by Th19;
  end;
  case
    H is negative;
    hence thesis by Th20;
  end;
  case
    H is conjunctive;
    hence thesis by Th21;
  end;
  case
    H is universal;
    hence thesis by Th22;
  end;
end;

theorem
  H.1 = 0 implies H is being_equality by Th23;

theorem
  H.1 = 1 implies H is being_membership by Th23;

theorem
  H.1 = 2 implies H is negative by Th23;

theorem
  H.1 = 3 implies H is conjunctive by Th23;

theorem
  H.1 = 4 implies H is universal by Th23;

reserve sq,sq9 for FinSequence;

theorem Th29:
  H = F^sq implies H = F
proof
  defpred P[Nat] means for H,F,sq st len H = $1 & H = F^sq holds H = F;
  for n being Nat st for k being Nat st k < n for H,F,sq st len H = k & H
  = F^sq holds H = F for H,F,sq st len H = n & H = F^sq holds H = F
  proof
    let n be Nat such that
A1: for k be Nat st k < n for H,F,sq st len H = k & H = F^sq holds H = F;
    let H,F,sq such that
A2: len H = n and
A3: H = F^sq;
    3 <= len F by Th13;
    then dom F = Seg len F & 1 <= len F by FINSEQ_1:def 3,XXREAL_0:2;
    then
A4: 1 in dom F by FINSEQ_1:1;
A5: now
A6:   len <*2*> = 1 by FINSEQ_1:40;
      assume
A7:   H is negative;
      then consider H1 such that
A8:   H = 'not' H1 by Def12;
      (F^sq).1 = 2 by A3,A7,Th20;
      then F.1 = 2 by A4,FINSEQ_1:def 7;
      then F is negative by Th23;
      then consider F1 such that
A9:   F = 'not' F1 by Def12;
      len <*2*> + len H1 = len H by A8,FINSEQ_1:22;
      then
A10:  len H1 < len H by A6,NAT_1:13;
      <*2*>^F1^sq = <*2*>^(F1^sq) by FINSEQ_1:32;
      then H1 = F1^sq by A3,A8,A9,FINSEQ_1:33;
      hence thesis by A1,A2,A8,A9,A10;
    end;
A11: now
      assume
A12:  H is conjunctive;
      then consider G1,G such that
A13:  H = G1 '&' G by Def13;
A14:  len G + (1 + len G1) = len G + 1 + len G1;
A15:  len(<*3*>^G1) = len <*3*> + len G1 & len <*3*> = 1 by FINSEQ_1:22,40;
      len(<*3*>^G1) + len G = len H by A13,FINSEQ_1:22;
      then len G + 1 <= len H by A15,A14,NAT_1:11;
      then
A16:  len G < len H by NAT_1:13;
      (F^sq).1 = 3 by A3,A12,Th21;
      then F.1 = 3 by A4,FINSEQ_1:def 7;
      then F is conjunctive by Th23;
      then consider F1,H1 such that
A17:  F = F1 '&' H1 by Def13;
A18:  now
A19:    len F1 + 1 + len H1 + len sq = len F1 + 1 + (len H1 + len sq);
        given sq9 such that
A20:    F1 = G1^sq9;
A21:    len(F^sq) = len F + len sq & len <*3*> = 1 by FINSEQ_1:22,40;
        len(<*3*>^F1) = len <*3*> + len F1 & len F = len(<*3*>^F1) + len
        H1 by A17,FINSEQ_1:22;
        then len F1 + 1 <= len H by A3,A21,A19,NAT_1:11;
        then len F1 < len H by NAT_1:13;
        hence F1 = G1 by A1,A2,A20;
      end;
A22:  <*3*>^F1^H1 = <*3*>^(F1^H1) & <*3*>^(F1^H1)^sq = <*3*>^(F1^H1^sq)
      by FINSEQ_1:32;
A23:  now
        given sq9 such that
A24:    G1 = F1^sq9;
A25:    len <*3*> = 1 by FINSEQ_1:40;
        len(<*3*>^G1) + len G = len H & len(<*3*>^G1) = len <*3*> + len
        G1 by A13,FINSEQ_1:22;
        then len G1 + 1 <= len H by A25,NAT_1:11;
        then len G1 < len H by NAT_1:13;
        hence G1 = F1 by A1,A2,A24;
      end;
A26:  F1^H1^sq = F1^(H1^sq) by FINSEQ_1:32;
      <*3*>^G1^G = <*3*>^(G1^G) by FINSEQ_1:32;
      then
A27:  G1^G = F1^(H1^sq) by A3,A13,A17,A22,A26,FINSEQ_1:33;
      then len F1 <= len G1 implies ex sq9 st G1 = F1^sq9 by FINSEQ_1:47;
      then G = H1^sq by A27,A23,A18,FINSEQ_1:33,47;
      hence thesis by A1,A2,A3,A17,A22,A26,A16;
    end;
A28: now
      assume
A29:  H is universal;
      then consider x,H1 such that
A30:  H = All(x,H1) by Def14;
A31:  <*4*>^<*x*> = <*4,x*> by FINSEQ_1:def 9;
A32:  len <*4,x*> = 2 & 1 + (1 + len H1) = 1 + len H1 + 1 by FINSEQ_1:44;
      len(<*4*>^<*x*>) + len H1 = len H by A30,FINSEQ_1:22;
      then len H1 + 1 <= len H by A32,A31,NAT_1:11;
      then
A33:  len H1 < len H by NAT_1:13;
      (F^sq).1 = 4 by A3,A29,Th22;
      then F.1 = 4 by A4,FINSEQ_1:def 7;
      then F is universal by Th23;
      then consider y,F1 such that
A34:  F = All(y,F1) by Def14;
A35:  (<*x*>^H1).1 = x & (<*y*>^(F1^sq)).1 = y by FINSEQ_1:41;
A36:  <*4*>^<*y*>^F1^sq = <*4*>^<*y*>^(F1^sq) by FINSEQ_1:32;
      <*4*>^<*x*>^H1 = <*4*>^(<*x*>^H1) & <*4*>^<*y*>^(F1^sq) = <*4*>^(<*
      y*>^(F1^ sq)) by FINSEQ_1:32;
      then <*x*>^H1 = <*y*>^(F1^sq) by A3,A30,A34,A36,FINSEQ_1:33;
      then H1 = F1^sq by A35,FINSEQ_1:33;
      hence thesis by A1,A2,A3,A34,A36,A33;
    end;
A37: len F + len sq = len(F^sq) by FINSEQ_1:22;
    now
A38:  3 <= len F by Th13;
      assume H is atomic;
      then
A39:  len H = 3 by Th11;
      then len F <= 3 by A3,A37,NAT_1:11;
      then 3 + len sq = 3 + 0 by A3,A37,A39,A38,XXREAL_0:1;
      then sq = {};
      hence thesis by A3,FINSEQ_1:34;
    end;
    hence thesis by A5,A28,A11,Th10;
  end;
  then
A40: for k being Nat st for n being Nat st n < k holds P[n] holds P[k];
A41: for n being Nat holds P[n] from NAT_1:sch 4(A40);
  len H = len H;
  hence thesis by A41;
end;

theorem Th30:
  H '&' G = H1 '&' G1 implies H = H1 & G = G1
proof
  assume
A1: H '&' G = H1 '&' G1;
  <*3*>^H^G = <*3*>^(H^G) & <*3*>^H1^G1 = <*3*>^(H1^G1) by FINSEQ_1:32;
  then
A2: H^G = H1^G1 by A1,FINSEQ_1:33;
  then
A3: len H1 <= len H implies ex sq st H = H1^sq by FINSEQ_1:47;
A4: len H <= len H1 implies ex sq st H1 = H^sq by A2,FINSEQ_1:47;
  hence H = H1 by A3,Th29;
  (ex sq st H1 = H^sq) implies H1 = H by Th29;
  hence thesis by A1,A3,A4,Th29,FINSEQ_1:33;
end;

theorem Th31:
  F 'or' G = F1 'or' G1 implies F = F1 & G = G1
proof
  assume F 'or' G = F1 'or' G1;
  then 'not' F '&' 'not' G = 'not' F1 '&' 'not' G1 by FINSEQ_1:33;
  then 'not' F = 'not' F1 & 'not' G = 'not' G1 by Th30;
  hence thesis by FINSEQ_1:33;
end;

theorem Th32:
  F => G = F1 => G1 implies F = F1 & G = G1
proof
  assume F => G = F1 => G1;
  then
A1: F '&' 'not' G = F1 '&' 'not' G1 by FINSEQ_1:33;
  hence F = F1 by Th30;
  'not' G = 'not' G1 by A1,Th30;
  hence thesis by FINSEQ_1:33;
end;

theorem Th33:
  F <=> G = F1 <=> G1 implies F = F1 & G = G1
proof
  assume F <=> G = F1 <=> G1;
  then F => G = F1=> G1 by Th30;
  hence thesis by Th32;
end;

theorem Th34:
  Ex(x,H) = Ex(y,G) implies x = y & H = G
proof
  assume Ex(x,H) = Ex(y,G);
  then
A1: All(x,'not' H) = All(y,'not' G) by FINSEQ_1:33;
  then 'not' H = 'not' G by Th3;
  hence thesis by A1,Th3,FINSEQ_1:33;
end;

::
::             The Select Function of ZF-fomrulae
::

definition
  let H;
  assume
A1: H is atomic;
  func Var1 H -> Variable equals
  :Def28:
  H.2;
  coherence
  proof
A2: (ex x,y st H = x 'in' y) implies ex k, x, y st H = <*k*>^<*x*>^<*y*>;
A3: (ex x,y st H = x '=' y) implies ex k,x, y st H = <*k*>^<*x*>^<*y*>;
    H is being_equality or H is being_membership by A1,Def15;
    then consider k,x,y such that
A4: H = <*k*>^<*x*>^<*y*> by A3,A2,Def10,Def11;
    H = <* k,x,y *> by A4,FINSEQ_1:def 10;
    hence thesis by FINSEQ_1:45;
  end;
  func Var2 H -> Variable equals
  :Def29:
  H.3;
  coherence
  proof
A5: (ex x,y st H = x 'in' y) implies ex k, x, y st H = <*k*>^<*x*>^<*y*>;
A6: (ex x,y st H = x '=' y) implies ex k, x, y st H = <*k*>^<*x*>^<*y*>;
    H is being_equality or H is being_membership by A1,Def15;
    then consider k,x,y such that
A7: H = <*k*>^<*x*>^<*y*> by A6,A5,Def10,Def11;
    H = <* k,x,y *> by A7,FINSEQ_1:def 10;
    hence thesis by FINSEQ_1:45;
  end;
end;

theorem
  H is atomic implies Var1 H = H.2 & Var2 H = H.3 by Def28,Def29;

theorem Th36:
  H is being_equality implies H = (Var1 H) '=' Var2 H
proof
  assume
A1: H is being_equality;
  then consider x,y such that
A2: H = x '=' y by Def10;
  <*0*>^<*x*>^<*y*> = <*0,x,y*> by FINSEQ_1:def 10;
  then
A3: H.2 = x & H.3 = y by A2,FINSEQ_1:45;
A4: H is atomic by A1,Def15;
  then H.2 = Var1 H by Def28;
  hence thesis by A2,A4,A3,Def29;
end;

theorem Th37:
  H is being_membership implies H = (Var1 H) 'in' Var2 H
proof
  assume
A1: H is being_membership;
  then consider x,y such that
A2: H = x 'in' y by Def11;
  <*1*>^<*x*>^<*y*> = <*1,x,y*> by FINSEQ_1:def 10;
  then
A3: H.2 = x & H.3 = y by A2,FINSEQ_1:45;
A4: H is atomic by A1,Def15;
  then H.2 = Var1 H by Def28;
  hence thesis by A2,A4,A3,Def29;
end;

definition
  let H;
  assume
A1: H is negative;
  func the_argument_of H -> ZF-formula means
  :Def30:
  'not' it = H;
  existence by A1,Def12;
  uniqueness by FINSEQ_1:33;
end;

definition
  let H;
  assume
A1: H is conjunctive or H is disjunctive;
  func the_left_argument_of H -> ZF-formula means
  :Def31:
  ex H1 st it '&' H1 = H if H is conjunctive otherwise ex H1 st it 'or' H1 = H;
  existence by A1,Def13,Def20;
  uniqueness by Th30,Th31;
  consistency;
  func the_right_argument_of H -> ZF-formula means
  :Def32:
  ex H1 st H1 '&' it = H if H is conjunctive otherwise ex H1 st H1 'or' it = H;
  existence
  proof
    thus H is conjunctive implies ex G,H1 st H1 '&' G = H
    proof
      assume H is conjunctive;
      then consider G,F such that
A2:   G '&' F = H by Def13;
      take F;
      thus thesis by A2;
    end;
    thus not H is conjunctive implies ex G,H1 st H1 'or' G = H
    proof
      assume not H is conjunctive;
      then consider G,F such that
A3:   G 'or' F = H by A1,Def20;
      take F;
      thus thesis by A3;
    end;
  end;
  uniqueness by Th30,Th31;
  consistency;
end;

theorem
  H is conjunctive implies (F = the_left_argument_of H iff ex G st F '&'
G = H) & (F = the_right_argument_of H iff ex G st G '&' F = H) by Def31,Def32;

theorem Th39:
  H is disjunctive implies (F = the_left_argument_of H iff ex G st
  F 'or' G = H) & (F = the_right_argument_of H iff ex G st G 'or' F = H)
proof
  assume
A1: H is disjunctive;
  then ex F,G st H = F 'or' G by Def20;
  then H.1 = 2 by FINSEQ_1:41;
  then not H is conjunctive by Th21;
  hence thesis by A1,Def31,Def32;
end;

theorem Th40:
  H is conjunctive implies H = (the_left_argument_of H) '&'
  the_right_argument_of H
proof
  assume
A1: H is conjunctive;
  then ex F1 st H = (the_left_argument_of H) '&' F1 by Def31;
  hence thesis by A1,Def32;
end;

theorem
  H is disjunctive implies H = (the_left_argument_of H) 'or'
  the_right_argument_of H
proof
  assume
A1: H is disjunctive;
  then ex F1 st H = (the_left_argument_of H) 'or' F1 by Th39;
  hence thesis by A1,Th39;
end;

definition
  let H;
  assume
A1: H is universal or H is existential;
  func bound_in H -> Variable means
  :Def33:
  ex H1 st All(it,H1) = H if H is universal otherwise ex H1 st Ex(it,H1) = H;
  existence by A1,Def14,Def23;
  uniqueness by Th3,Th34;
  consistency;
  func the_scope_of H -> ZF-formula means
  :Def34:
  ex x st All(x,it) = H if H is universal otherwise ex x st Ex(x,it) = H;
  existence
  proof
    thus H is universal implies ex H1,x st All(x,H1) = H
    proof
      assume H is universal;
      then consider x,G such that
A2:   All(x,G) = H by Def14;
      take G;
      thus thesis by A2;
    end;
    thus not H is universal implies ex H1,x st Ex(x,H1) = H
    proof
      assume not H is universal;
      then consider x,G such that
A3:   Ex(x,G) = H by A1,Def23;
      take G;
      thus thesis by A3;
    end;
  end;
  uniqueness by Th3,Th34;
  consistency;
end;

theorem
  H is universal implies (x = bound_in H iff ex H1 st All(x,H1) = H) & (
  H1 = the_scope_of H iff ex x st All(x,H1) = H) by Def33,Def34;

theorem Th43:
  H is existential implies (x = bound_in H iff ex H1 st Ex(x,H1) =
  H) & (H1 = the_scope_of H iff ex x st Ex(x,H1) = H)
proof
  assume
A1: H is existential;
  then ex y,F st H = Ex(y,F) by Def23;
  then H.1 = 2 by FINSEQ_1:41;
  then not H is universal by Th22;
  hence thesis by A1,Def33,Def34;
end;

theorem Th44:
  H is universal implies H = All(bound_in H,the_scope_of H)
proof
  assume
A1: H is universal;
  then ex x st H = All(x,the_scope_of H) by Def34;
  hence thesis by A1,Def33;
end;

theorem
  H is existential implies H = Ex(bound_in H,the_scope_of H)
proof
  assume
A1: H is existential;
  then ex x st H = Ex(x,the_scope_of H) by Th43;
  hence thesis by A1,Th43;
end;

definition
  let H;
  assume
A1: H is conditional;
  func the_antecedent_of H -> ZF-formula means
  :Def35:
  ex H1 st H = it => H1;
  existence by A1,Def21;
  uniqueness by Th32;
  func the_consequent_of H -> ZF-formula means
  :Def36:
  ex H1 st H = H1 => it;
  existence
  proof
    consider F,G such that
A2: H = F => G by A1,Def21;
    take G,F;
    thus thesis by A2;
  end;
  uniqueness by Th32;
end;

theorem
  H is conditional implies (F = the_antecedent_of H iff ex G st H = F =>
  G) & (F = the_consequent_of H iff ex G st H = G => F) by Def35,Def36;

theorem
  H is conditional implies H = (the_antecedent_of H) => the_consequent_of H
proof
  assume
A1: H is conditional;
  then ex F st H = (the_antecedent_of H) => F by Def35;
  hence thesis by A1,Def36;
end;

definition
  let H;
  assume
A1: H is biconditional;
  func the_left_side_of H -> ZF-formula means
  :Def37:
  ex H1 st H = it <=> H1;
  existence by A1,Def22;
  uniqueness by Th33;
  func the_right_side_of H -> ZF-formula means
  :Def38:
  ex H1 st H = H1 <=> it;
  existence
  proof
    consider F,G such that
A2: H = F <=> G by A1,Def22;
    take G,F;
    thus thesis by A2;
  end;
  uniqueness by Th33;
end;

theorem
  H is biconditional implies (F = the_left_side_of H iff ex G st H = F
  <=> G) & (F = the_right_side_of H iff ex G st H = G <=> F) by Def37,Def38;

theorem
  H is biconditional implies H = (the_left_side_of H) <=> the_right_side_of H
proof
  assume
A1: H is biconditional;
  then ex F st H = (the_left_side_of H) <=> F by Def37;
  hence thesis by A1,Def38;
end;

::
::         The Immediate Constituents of ZF-formulae
::

definition
  let H,F;
  pred H is_immediate_constituent_of F means
  :Def39:
  F = 'not' H or ( ex H1 st
  F = H '&' H1 or F = H1 '&' H ) or ex x st F = All(x,H);
end;

theorem Th50:
  not H is_immediate_constituent_of x '=' y
proof
  assume H is_immediate_constituent_of x '=' y;
  then
A1: x '=' y = 'not' H or ( ex H1 st x '=' y = H '&' H1 or x '=' y = H1 '&' H
  ) or ex z st x '=' y = All(z,H) by Def39;
  (x '=' y).1 = 0 by Th15;
  hence contradiction by A1,Th16,Th17,FINSEQ_1:41;
end;

theorem Th51:
  not H is_immediate_constituent_of x 'in' y
proof
  assume H is_immediate_constituent_of x 'in' y;
  then
A1: x 'in' y = 'not' H or ( ex H1 st x 'in' y = H '&' H1 or x 'in' y = H1
  '&' H ) or ex z st x 'in' y = All(z,H) by Def39;
  (x 'in' y).1 = 1 by Th15;
  hence contradiction by A1,Th16,Th17,FINSEQ_1:41;
end;

theorem Th52:
  F is_immediate_constituent_of 'not' H iff F = H
proof
  thus F is_immediate_constituent_of 'not' H implies F = H
  proof
A1: now
      given x such that
A2:   'not' H = All(x,F);
      ('not' H).1 = 2 by FINSEQ_1:41;
      hence contradiction by A2,Th17;
    end;
A3: now
      given H1 such that
A4:   'not' H = F '&' H1 or 'not' H = H1 '&' F;
      ('not' H).1 = 2 by FINSEQ_1:41;
      hence contradiction by A4,Th16;
    end;
    assume F is_immediate_constituent_of 'not' H;
    then
    'not' H = 'not' F or ( ex H1 st 'not' H = F '&' H1 or 'not' H = H1 '&'
    F ) or ex x st 'not' H = All(x,F) by Def39;
    hence thesis by A3,A1,FINSEQ_1:33;
  end;
  thus thesis by Def39;
end;

theorem Th53:
  F is_immediate_constituent_of G '&' H iff F = G or F = H
proof
  thus F is_immediate_constituent_of G '&' H implies F = G or F = H
  proof
A1: now
      given x such that
A2:   G '&' H = All(x,F);
      (G '&' H).1 = 3 by Th16;
      hence contradiction by A2,Th17;
    end;
A3: now
      assume
A4:   G '&' H = 'not' F;
      (G '&' H).1 = 3 by Th16;
      hence contradiction by A4,FINSEQ_1:41;
    end;
    assume F is_immediate_constituent_of G '&' H;
    then ex H1 st G '&' H = F '&' H1 or G '&' H = H1 '&' F by A3,A1,Def39;
    hence thesis by Th30;
  end;
  assume F = G or F = H;
  hence thesis by Def39;
end;

theorem Th54:
  F is_immediate_constituent_of All(x,H) iff F = H
proof
  thus F is_immediate_constituent_of All(x,H) implies F = H
  proof
A1: now
      given G such that
A2:   All(x,H) = F '&' G or All(x,H) = G '&' F;
      (F '&' G).1 = 3 & (G '&' F).1 = 3 by Th16;
      hence contradiction by A2,Th17;
    end;
A3: now
      assume
A4:   All(x,H) = 'not' F;
      All(x,H).1 = 4 by Th17;
      hence contradiction by A4,FINSEQ_1:41;
    end;
    assume F is_immediate_constituent_of All(x,H);
    then ex y st All(x,H) = All(y,F) by A3,A1,Def39;
    hence thesis by Th3;
  end;
  thus thesis by Def39;
end;

theorem
  H is atomic implies not F is_immediate_constituent_of H
proof
A1: now
    assume H is being_equality;
    then H = (Var1 H) '=' Var2 H by Th36;
    hence thesis by Th50;
  end;
A2: now
    assume H is being_membership;
    then H = (Var1 H) 'in' Var2 H by Th37;
    hence thesis by Th51;
  end;
  assume H is atomic;
  hence thesis by A1,A2,Def15;
end;

theorem Th56:
  H is negative implies (F is_immediate_constituent_of H iff F =
  the_argument_of H)
proof
  assume H is negative;
  then H = 'not' the_argument_of H by Def30;
  hence thesis by Th52;
end;

theorem Th57:
  H is conjunctive implies (F is_immediate_constituent_of H iff F
  = the_left_argument_of H or F = the_right_argument_of H)
proof
  assume H is conjunctive;
  then H = (the_left_argument_of H) '&' the_right_argument_of H by Th40;
  hence thesis by Th53;
end;

theorem Th58:
  H is universal implies (F is_immediate_constituent_of H iff F =
  the_scope_of H)
proof
  assume H is universal;
  then H = All(bound_in H,the_scope_of H) by Th44;
  hence thesis by Th54;
end;

::
::    The Subformulae and The Proper Subformulae of ZF-formulae
::

reserve L,L9 for FinSequence;

definition
  let H,F;
  pred H is_subformula_of F means
  :Def40:
  ex n,L st 1 <= n & len L = n & L.1 =
  H & L.n = F & for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 &
  H1 is_immediate_constituent_of F1;
end;

theorem Th59:
  H is_subformula_of H
proof
  take 1 , <*H*>;
  thus 1 <= 1;
  thus len <*H*> = 1 by FINSEQ_1:40;
  thus <*H*>.1 = H & <*H*>.1 = H by FINSEQ_1:def 8;
  thus thesis;
end;

definition
  let H,F;
  pred H is_proper_subformula_of F means
  :Def41:
  H is_subformula_of F & H <> F;
end;

theorem Th60:
  H is_immediate_constituent_of F implies len H < len F
proof
A1: now
    assume F = 'not' H;
    then len F = len <*2*> + len H by FINSEQ_1:22
      .= len H + 1 by FINSEQ_1:40;
    hence thesis by NAT_1:13;
  end;
A2: now
    given H1 such that
A3: F = H '&' H1 or F = H1 '&' H;
A4: len(<*3*>^H1^H) = len(<*3*>^(H1^H)) by FINSEQ_1:32
      .= len <*3*> + len(H1^H) by FINSEQ_1:22
      .= 1 + len(H1^H) by FINSEQ_1:40
      .= 1 + (len H + len H1) by FINSEQ_1:22
      .= 1 + len H + len H1;
    len(<*3*>^H^H1) = len(<*3*>^H) + len H1 by FINSEQ_1:22
      .= len <*3*> + len H + len H1 by FINSEQ_1:22
      .= 1 + len H + len H1 by FINSEQ_1:40;
    then 1 + len H <= len F by A3,A4,NAT_1:11;
    hence thesis by NAT_1:13;
  end;
A5: now
    given x such that
A6: F = All(x,H);
    len F = len(<*4*>^<*x*>) + len H by A6,FINSEQ_1:22
      .= len <*4*> + len <*x*> + len H by FINSEQ_1:22
      .= 1 + len <*x*> + len H by FINSEQ_1:40
      .= 1 + 1 + len H by FINSEQ_1:40
      .= (1 + len H) + 1;
    then 1 + len H <= len F by NAT_1:11;
    hence thesis by NAT_1:13;
  end;
  assume H is_immediate_constituent_of F;
  hence thesis by A1,A2,A5,Def39;
end;

theorem Th61:
  H is_immediate_constituent_of F implies H is_proper_subformula_of F
proof
  assume
A1: H is_immediate_constituent_of F;
  thus H is_subformula_of F
  proof
    take n = 2 , L = <* H,F *>;
    thus 1 <= n;
    thus len L = n by FINSEQ_1:44;
    thus L.1 = H & L.n = F by FINSEQ_1:44;
    let k;
    assume that
A2: 1 <= k and
A3: k < n;
    take H,F;
    k < 1 + 1 by A3;
    then k <= 1 by NAT_1:13;
    then k = 1 by A2,XXREAL_0:1;
    hence L.k = H & L.(k + 1) = F by FINSEQ_1:44;
    thus thesis by A1;
  end;
  assume H = F;
  then len H = len F;
  hence contradiction by A1,Th60;
end;

theorem Th62:
  H is_proper_subformula_of F implies len H < len F
proof
  assume H is_subformula_of F;
  then consider n,L such that
A1: 1 <= n and
  len L = n and
A2: L.1 = H and
A3: L.n = F and
A4: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
  is_immediate_constituent_of F1 by Def40;
  defpred P[Element of NAT] means 1 <= $1 & $1 < n implies for H1 st L.($1 + 1
  ) = H1 holds len H < len H1;
A5: for k st P[k] holds P[k + 1]
  proof
    let k such that
A6: 1 <= k & k < n implies for H1 st L.(k + 1) = H1 holds len H < len H1 and
A7: 1 <= k + 1 and
A8: k + 1 < n;
    consider F1,G such that
A9: L.(k + 1) = F1 and
A10: L.(k + 1 + 1) = G & F1 is_immediate_constituent_of G by A4,A7,A8;
    let H1 such that
A11: L.(k + 1 + 1) = H1;
A12: now
      given m be Nat such that
A13:  k = m + 1;
      len H < len F1 by A6,A8,A9,A13,NAT_1:11,13;
      hence thesis by A11,A10,Th60,XXREAL_0:2;
    end;
    k = 0 implies len H < len H1 by A2,A11,A9,A10,Th60;
    hence thesis by A12,NAT_1:6;
  end;
  assume H <> F;
  then 1 < n by A1,A2,A3,XXREAL_0:1;
  then 1 + 1 <= n by NAT_1:13;
  then consider k be Nat such that
A14: n = 2 + k by NAT_1:10;
A15: P[0];
A16: for k holds P[k] from NAT_1:sch 1(A15,A5);
  reconsider k as Element of NAT by ORDINAL1:def 12;
A17: 1 + 1 + k = (1 + k) + 1;
  then 1 + k < n by A14,NAT_1:13;
  hence thesis by A3,A16,A14,A17,NAT_1:11;
end;

theorem Th63:
  H is_proper_subformula_of F implies ex G st G is_immediate_constituent_of F
proof
  assume H is_subformula_of F;
  then consider n,L such that
A1: 1 <= n and
  len L = n and
A2: L.1 = H and
A3: L.n = F and
A4: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
  is_immediate_constituent_of F1 by Def40;
  assume H <> F;
  then 1 < n by A1,A2,A3,XXREAL_0:1;
  then 1 + 1 <= n by NAT_1:13;
  then consider k be Nat such that
A5: n = 2 + k by NAT_1:10;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  1 + 1 + k = (1 + k) + 1;
  then 1 + k < n by A5,NAT_1:13;
  then consider H1,F1 such that
  L.(1 + k) = H1 and
A6: L.(1 + k + 1) = F1 & H1 is_immediate_constituent_of F1 by A4,NAT_1:11;
  take H1;
  thus thesis by A3,A5,A6;
end;

reserve j,j1 for Element of NAT;

theorem Th64:
  F is_proper_subformula_of G & G is_proper_subformula_of H
  implies F is_proper_subformula_of H
proof
  assume that
A1: F is_subformula_of G and
A2: F <> G and
A3: G is_subformula_of H and
A4: G <> H;
  consider m,L9 such that
A5: 1 <= m and
A6: len L9 = m and
A7: L9.1 = G and
A8: L9.m = H and
A9: for k st 1 <= k & k < m ex H1,F1 st L9.k = H1 & L9.(k + 1) = F1 &
  H1 is_immediate_constituent_of F1 by A3,Def40;
  consider n,L such that
A10: 1 <= n and
A11: len L = n and
A12: L.1 = F and
A13: L.n = G and
A14: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
  is_immediate_constituent_of F1 by A1,Def40;
  1 < n by A2,A10,A12,A13,XXREAL_0:1;
  then 1 + 1 <= n by NAT_1:13;
  then consider k be Nat such that
A15: n = 2 + k by NAT_1:10;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
  thus F is_subformula_of H
  proof
    take l = 1 + k + m, K = L1^L9;
A16: 1 + k + m - (1 + k) = m;
    m <= m + (1 + k) by NAT_1:11;
    hence 1 <= l by A5,XXREAL_0:2;
    1 + 1 + k = 1 + k + 1;
    then
A17: 1 + k <= n by A15,NAT_1:11;
    then
A18: len L1 = 1 + k by A11,FINSEQ_1:17;
    hence
A19: len K = l by A6,FINSEQ_1:22;
A20: now
      let j;
      assume 1 <= j & j <= 1 + k;
      then
A21:  j in Seg(1 + k) by FINSEQ_1:1;
      then j in dom L1 by A11,A17,FINSEQ_1:17;
      then K.j = L1.j by FINSEQ_1:def 7;
      hence K.j = L.j by A21,FUNCT_1:49;
    end;
    1 <= 1 + k by NAT_1:11;
    hence K.1 = F by A12,A20;
    len L1 + 1 <= len L1 + m by A5,XREAL_1:7;
    then len L1 < l by A18,NAT_1:13;
    then K.l = L9.(l - len L1) by A19,FINSEQ_1:24;
    hence K.l = H by A11,A8,A17,A16,FINSEQ_1:17;
    let j such that
A22: 1 <= j and
A23: j < l;
    j + 0 <= j + 1 by XREAL_1:7;
    then
A24: 1 <= j + 1 by A22,XXREAL_0:2;
A25: now
      assume
A26:  j < 1 + k;
      then
A27:  j + 1 <= 1 + k by NAT_1:13;
      then j + 1 <= n by A17,XXREAL_0:2;
      then j < n by NAT_1:13;
      then consider F1,G1 such that
A28:  L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A14,A22;
      take F1, G1;
      thus K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A20
,A22,A24,A26,A27,A28;
    end;
A29: now
A30:  j + 1 <= l by A23,NAT_1:13;
      assume
A31:  1 + k < j;
      then
A32:  1 + k < j + 1 by NAT_1:13;
      1 + k + 1 <= j by A31,NAT_1:13;
      then consider j1 be Nat such that
A33:  j = 1 + k + 1 + j1 by NAT_1:10;
      reconsider j1 as Element of NAT by ORDINAL1:def 12;
      j - (1 + k) < l - (1 + k) by A23,XREAL_1:9;
      then consider F1,G1 such that
A34:  L9.(1 + j1) = F1 & L9.(1 + j1 + 1) = G1 & F1
      is_immediate_constituent_of G1 by A9,A33,NAT_1:11;
      take F1, G1;
A35:  1 + j1 + (1 + k) - (1 + k) = 1 + j1 + (1 + k) + -(1 + k);
      j + 1 - len L1 = 1 + (j + -len L1)
        .= 1 + j1 + 1 by A11,A17,A33,A35,FINSEQ_1:17;
      hence K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by
A18,A19,A23,A31,A32,A30,A35,A34,FINSEQ_1:24;
    end;
    now
A36:  j + 1 <= l & j + 1 - j = j + 1 + -j by A23,NAT_1:13;
      assume
A37:  j = 1 + k;
      then j < 1 + k + 1 by NAT_1:13;
      then consider F1,G1 such that
A38:  L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1
      by A14,A15,A22;
      take F1, G1;
      1 + k < j + 1 by A37,NAT_1:13;
      hence
      K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A13,A7
,A15,A18,A19,A20,A22,A37,A36,A38,FINSEQ_1:24;
    end;
    hence thesis by A25,A29,XXREAL_0:1;
  end;
  assume
A39: F = H;
  F is_proper_subformula_of G by A1,A2,Def41;
  then
A40: len F < len G by Th62;
  G is_proper_subformula_of H by A3,A4,Def41;
  hence contradiction by A39,A40,Th62;
end;

theorem Th65:
  F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H
proof
  assume that
A1: F is_subformula_of G and
A2: G is_subformula_of H;
  now
    assume F <> G;
    then
A3: F is_proper_subformula_of G by A1,Def41;
    now
      assume G <> H;
      then G is_proper_subformula_of H by A2,Def41;
      then F is_proper_subformula_of H by A3,Th64;
      hence thesis by Def41;
    end;
    hence thesis by A1;
  end;
  hence thesis by A2;
end;

theorem
  G is_subformula_of H & H is_subformula_of G implies G = H
proof
  assume that
A1: G is_subformula_of H and
A2: H is_subformula_of G;
  assume
A3: G <> H;
  then G is_proper_subformula_of H by A1,Def41;
  then
A4: len G < len H by Th62;
  H is_proper_subformula_of G by A2,A3,Def41;
  hence contradiction by A4,Th62;
end;

theorem Th67:
  not F is_proper_subformula_of x '=' y
proof
  assume F is_proper_subformula_of x '=' y;
  then ex G st G is_immediate_constituent_of x '=' y by Th63;
  hence contradiction by Th50;
end;

theorem Th68:
  not F is_proper_subformula_of x 'in' y
proof
  assume F is_proper_subformula_of x 'in' y;
  then ex G st G is_immediate_constituent_of x 'in' y by Th63;
  hence contradiction by Th51;
end;

theorem Th69:
  F is_proper_subformula_of 'not' H implies F is_subformula_of H
proof
  assume that
A1: F is_subformula_of 'not' H and
A2: F <> 'not' H;
  consider n,L such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = F and
A6: L.n = 'not' H and
A7: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
  is_immediate_constituent_of F1 by A1,Def40;
  1 < n by A2,A3,A5,A6,XXREAL_0:1;
  then 1 + 1 <= n by NAT_1:13;
  then consider k be Nat such that
A8: n = 2 + k by NAT_1:10;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
  take m = 1 + k, L1;
  thus
A9: 1 <= m by NAT_1:11;
  1 + k <= 1 + k + 1 by NAT_1:11;
  hence len L1 = m by A4,A8,FINSEQ_1:17;
A10: now
    let j;
    assume 1 <= j & j <= m;
    then j in { j1 : 1 <= j1 & j1 <= 1 + k };
    then j in Seg(1 + k) by FINSEQ_1:def 1;
    hence L1.j = L.j by FUNCT_1:49;
  end;
  hence L1.1 = F by A5,A9;
  m < m + 1 by NAT_1:13;
  then consider F1,G1 such that
A11: L.m = F1 and
A12: L.(m + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A8,NAT_1:11;
  F1 = H by A6,A8,A12,Th52;
  hence L1.m = H by A9,A10,A11;
  let j;
  assume that
A13: 1 <= j and
A14: j < m;
  m <= m + 1 by NAT_1:11;
  then j < n by A8,A14,XXREAL_0:2;
  then consider F1,G1 such that
A15: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A13;
  take F1,G1;
  1 <= 1 + j & j + 1 <= m by A13,A14,NAT_1:13;
  hence thesis by A10,A13,A14,A15;
end;

theorem Th70:
  F is_proper_subformula_of G '&' H implies F is_subformula_of G
  or F is_subformula_of H
proof
  assume that
A1: F is_subformula_of G '&' H and
A2: F <> G '&' H;
  consider n,L such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = F and
A6: L.n = G '&' H and
A7: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
  is_immediate_constituent_of F1 by A1,Def40;
  1 < n by A2,A3,A5,A6,XXREAL_0:1;
  then 1 + 1 <= n by NAT_1:13;
  then consider k be Nat such that
A8: n = 2 + k by NAT_1:10;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  1 + 1 + k = 1 + k + 1;
  then 1 + k < n by A8,NAT_1:13;
  then consider H1,G1 such that
A9: L.(1 + k) = H1 and
A10: L.(1 + k + 1) = G1 & H1 is_immediate_constituent_of G1 by A7,NAT_1:11;
  reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
  F is_subformula_of H1
  proof
    take m = 1 + k, L1;
    thus
A11: 1 <= m by NAT_1:11;
    1 + k <= 1 + k + 1 by NAT_1:11;
    hence len L1 = m by A4,A8,FINSEQ_1:17;
A12: now
      let j;
      assume 1 <= j & j <= m;
      then j in { j1 : 1 <= j1 & j1 <= 1 + k };
      then j in Seg(1 + k) by FINSEQ_1:def 1;
      hence L1.j = L.j by FUNCT_1:49;
    end;
    hence L1.1 = F by A5,A11;
    thus L1.m = H1 by A9,A11,A12;
    let j;
    assume that
A13: 1 <= j and
A14: j < m;
    m <= m + 1 by NAT_1:11;
    then j < n by A8,A14,XXREAL_0:2;
    then consider F1,G1 such that
A15: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A13;
    take F1,G1;
    1 <= 1 + j & j + 1 <= m by A13,A14,NAT_1:13;
    hence thesis by A12,A13,A14,A15;
  end;
  hence thesis by A6,A8,A10,Th53;
end;

theorem Th71:
  F is_proper_subformula_of All(x,H) implies F is_subformula_of H
proof
  assume that
A1: F is_subformula_of All(x,H) and
A2: F <> All(x,H);
  consider n,L such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = F and
A6: L.n = All(x,H) and
A7: for k st 1 <= k & k < n ex H1,F1 st L.k = H1 & L.(k + 1) = F1 & H1
  is_immediate_constituent_of F1 by A1,Def40;
  1 < n by A2,A3,A5,A6,XXREAL_0:1;
  then 1 + 1 <= n by NAT_1:13;
  then consider k be Nat such that
A8: n = 2 + k by NAT_1:10;
  reconsider k as Element of NAT by ORDINAL1:def 12;
  reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
  take m = 1 + k, L1;
  thus
A9: 1 <= m by NAT_1:11;
  1 + k <= 1 + k + 1 by NAT_1:11;
  hence len L1 = m by A4,A8,FINSEQ_1:17;
A10: now
    let j;
    assume 1 <= j & j <= m;
    then j in { j1 : 1 <= j1 & j1 <= 1 + k };
    then j in Seg(1 + k) by FINSEQ_1:def 1;
    hence L1.j = L.j by FUNCT_1:49;
  end;
  hence L1.1 = F by A5,A9;
  m < m + 1 by NAT_1:13;
  then consider F1,G1 such that
A11: L.m = F1 and
A12: L.(m + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A8,NAT_1:11;
  F1 = H by A6,A8,A12,Th54;
  hence L1.m = H by A9,A10,A11;
  let j;
  assume that
A13: 1 <= j and
A14: j < m;
  m <= m + 1 by NAT_1:11;
  then j < n by A8,A14,XXREAL_0:2;
  then consider F1,G1 such that
A15: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A13;
  take F1,G1;
  1 <= 1 + j & j + 1 <= m by A13,A14,NAT_1:13;
  hence thesis by A10,A13,A14,A15;
end;

theorem
  H is atomic implies not F is_proper_subformula_of H
proof
  assume H is atomic;
  then H is being_equality or H is being_membership by Def15;
  then H = (Var1 H) '=' Var2 H or H = (Var1 H) 'in' Var2 H by Th36,Th37;
  hence thesis by Th67,Th68;
end;

theorem
  H is negative implies the_argument_of H is_proper_subformula_of H
proof
  assume H is negative;
  then the_argument_of H is_immediate_constituent_of H by Th56;
  hence thesis by Th61;
end;

theorem
  H is conjunctive implies the_left_argument_of H
  is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H
proof
  assume H is conjunctive;
  then the_left_argument_of H is_immediate_constituent_of H &
  the_right_argument_of H is_immediate_constituent_of H by Th57;
  hence thesis by Th61;
end;

theorem
  H is universal implies the_scope_of H is_proper_subformula_of H
proof
  assume H is universal;
  then the_scope_of H is_immediate_constituent_of H by Th58;
  hence thesis by Th61;
end;

theorem Th76:
  H is_subformula_of x '=' y iff H = x '=' y
proof
  thus H is_subformula_of x '=' y implies H = x '=' y
  proof
    assume
A1: H is_subformula_of x '=' y;
    assume H <> x '=' y;
    then H is_proper_subformula_of x '=' y by A1,Def41;
    then ex F st F is_immediate_constituent_of x '=' y by Th63;
    hence contradiction by Th50;
  end;
  thus thesis by Th59;
end;

theorem Th77:
  H is_subformula_of x 'in' y iff H = x 'in' y
proof
  thus H is_subformula_of x 'in' y implies H = x 'in' y
  proof
    assume
A1: H is_subformula_of x 'in' y;
    assume H <> x 'in' y;
    then H is_proper_subformula_of x 'in' y by A1,Def41;
    then ex F st F is_immediate_constituent_of x 'in' y by Th63;
    hence contradiction by Th51;
  end;
  assume H = x 'in' y;
  hence thesis by Th59;
end;

::
::           The Set of Subformulae of ZF-formulae
::

definition
  let H;
  func Subformulae H -> set means
  :Def42:
  a in it iff ex F st F = a & F is_subformula_of H;
  existence
  proof
    defpred X[set] means ex F st F = $1 & F is_subformula_of H;
    consider X such that
A1: a in X iff a in NAT* & X[a] from XBOOLE_0:sch 1;
    take X;
    let a;
    thus a in X implies ex F st F = a & F is_subformula_of H by A1;
    given F such that
A2: F = a & F is_subformula_of H;
    F in NAT* by FINSEQ_1:def 11;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    let X,Y such that
A3: a in X iff ex F st F = a & F is_subformula_of H and
A4: a in Y iff ex F st F = a & F is_subformula_of H;
    now
      let a;
      thus a in X implies a in Y
      proof
        assume a in X;
        then ex F st F = a & F is_subformula_of H by A3;
        hence thesis by A4;
      end;
      assume a in Y;
      then ex F st F = a & F is_subformula_of H by A4;
      hence a in X by A3;
    end;
    hence thesis by TARSKI:1;
  end;
end;

theorem Th78:
  G in Subformulae H implies G is_subformula_of H
proof
  assume G in Subformulae H;
  then ex F st F = G & F is_subformula_of H by Def42;
  hence thesis;
end;

theorem
  F is_subformula_of H implies Subformulae F c= Subformulae H
proof
  assume
A1: F is_subformula_of H;
  let a;
  assume a in Subformulae F;
  then consider F1 such that
A2: F1 = a and
A3: F1 is_subformula_of F by Def42;
  F1 is_subformula_of H by A1,A3,Th65;
  hence thesis by A2,Def42;
end;

theorem Th80:
  Subformulae x '=' y = { x '=' y }
proof
  now
    let a;
    thus a in Subformulae x '=' y implies a in { x '=' y }
    proof
      assume a in Subformulae x '=' y;
      then consider F such that
A1:   F = a and
A2:   F is_subformula_of x '=' y by Def42;
      F = x '=' y by A2,Th76;
      hence thesis by A1,TARSKI:def 1;
    end;
    assume a in { x '=' y };
    then
A3: a = x '=' y by TARSKI:def 1;
    x '=' y is_subformula_of x '=' y by Th59;
    hence a in Subformulae x '=' y by A3,Def42;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th81:
  Subformulae x 'in' y = { x 'in' y }
proof
  now
    let a;
    thus a in Subformulae x 'in' y implies a in { x 'in' y }
    proof
      assume a in Subformulae x 'in' y;
      then consider F such that
A1:   F = a and
A2:   F is_subformula_of x 'in' y by Def42;
      F = x 'in' y by A2,Th77;
      hence thesis by A1,TARSKI:def 1;
    end;
    assume a in { x 'in' y };
    then
A3: a = x 'in' y by TARSKI:def 1;
    x 'in' y is_subformula_of x 'in' y by Th59;
    hence a in Subformulae x 'in' y by A3,Def42;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th82:
  Subformulae 'not' H = Subformulae H \/ { 'not' H }
proof
  now
    let a;
A1: now
      assume a in { 'not' H };
      then
A2:   a = 'not' H by TARSKI:def 1;
      'not' H is_subformula_of 'not' H by Th59;
      hence a in Subformulae 'not' H by A2,Def42;
    end;
    thus a in Subformulae 'not' H implies a in Subformulae H \/ { 'not' H }
    proof
      assume a in Subformulae 'not' H;
      then consider F such that
A3:   F = a and
A4:   F is_subformula_of 'not' H by Def42;
      now
        assume F <> 'not' H;
        then F is_proper_subformula_of 'not' H by A4,Def41;
        then F is_subformula_of H by Th69;
        hence a in Subformulae H by A3,Def42;
      end;
      then a in Subformulae H or a in { 'not' H } by A3,TARSKI:def 1;
      hence thesis by XBOOLE_0:def 3;
    end;
A5: now
      assume a in Subformulae H;
      then consider F such that
A6:   F = a and
A7:   F is_subformula_of H by Def42;
      H is_immediate_constituent_of 'not' H by Th52;
      then H is_proper_subformula_of 'not' H by Th61;
      then H is_subformula_of 'not' H by Def41;
      then F is_subformula_of 'not' H by A7,Th65;
      hence a in Subformulae 'not' H by A6,Def42;
    end;
    assume a in Subformulae H \/ { 'not' H };
    hence a in Subformulae 'not' H by A5,A1,XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th83:
  Subformulae (H '&' F) = Subformulae H \/ Subformulae F \/ { H '&' F }
proof
  now
    let a;
A1: a in Subformulae H \/ Subformulae F implies a in Subformulae H or a
    in Subformulae F by XBOOLE_0:def 3;
    thus a in Subformulae H '&' F implies a in Subformulae H \/ Subformulae F
    \/ { H '&' F }
    proof
      assume a in Subformulae H '&' F;
      then consider G such that
A2:   G = a and
A3:   G is_subformula_of H '&' F by Def42;
      now
        assume G <> H '&' F;
        then G is_proper_subformula_of H '&' F by A3,Def41;
        then G is_subformula_of H or G is_subformula_of F by Th70;
        then a in Subformulae H or a in Subformulae F by A2,Def42;
        hence a in Subformulae H \/ Subformulae F by XBOOLE_0:def 3;
      end;
      then a in Subformulae H \/ Subformulae F or a in { H '&' F } by A2,
TARSKI:def 1;
      hence thesis by XBOOLE_0:def 3;
    end;
A4: now
      assume a in { H '&' F };
      then
A5:   a = H '&' F by TARSKI:def 1;
      H '&' F is_subformula_of H '&' F by Th59;
      hence a in Subformulae H '&' F by A5,Def42;
    end;
A6: now
      assume a in Subformulae F;
      then consider G such that
A7:   G = a and
A8:   G is_subformula_of F by Def42;
      F is_immediate_constituent_of H '&' F by Th53;
      then F is_proper_subformula_of H '&' F by Th61;
      then F is_subformula_of H '&' F by Def41;
      then G is_subformula_of H '&' F by A8,Th65;
      hence a in Subformulae H '&' F by A7,Def42;
    end;
A9: now
      assume a in Subformulae H;
      then consider G such that
A10:  G = a and
A11:  G is_subformula_of H by Def42;
      H is_immediate_constituent_of H '&' F by Th53;
      then H is_proper_subformula_of H '&' F by Th61;
      then H is_subformula_of H '&' F by Def41;
      then G is_subformula_of H '&' F by A11,Th65;
      hence a in Subformulae H '&' F by A10,Def42;
    end;
    assume a in Subformulae H \/ Subformulae F \/ { H '&' F };
    hence a in Subformulae H '&' F by A1,A9,A6,A4,XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th84:
  Subformulae All(x,H) = Subformulae H \/ { All(x,H) }
proof
  now
    let a;
A1: now
      assume a in { All(x,H) };
      then
A2:   a = All(x,H) by TARSKI:def 1;
      All(x,H) is_subformula_of All(x,H) by Th59;
      hence a in Subformulae All(x,H) by A2,Def42;
    end;
    thus a in Subformulae All(x,H) implies a in Subformulae H \/ { All(x,H) }
    proof
      assume a in Subformulae All(x,H);
      then consider F such that
A3:   F = a and
A4:   F is_subformula_of All(x,H) by Def42;
      now
        assume F <> All(x,H);
        then F is_proper_subformula_of All(x,H) by A4,Def41;
        then F is_subformula_of H by Th71;
        hence a in Subformulae H by A3,Def42;
      end;
      then a in Subformulae H or a in { All(x,H) } by A3,TARSKI:def 1;
      hence thesis by XBOOLE_0:def 3;
    end;
A5: now
      assume a in Subformulae H;
      then consider F such that
A6:   F = a and
A7:   F is_subformula_of H by Def42;
      H is_immediate_constituent_of All(x,H) by Th54;
      then H is_proper_subformula_of All(x,H) by Th61;
      then H is_subformula_of All(x,H) by Def41;
      then F is_subformula_of All(x,H) by A7,Th65;
      hence a in Subformulae All(x,H) by A6,Def42;
    end;
    assume a in Subformulae H \/ { All(x,H) };
    hence a in Subformulae All(x,H) by A5,A1,XBOOLE_0:def 3;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  H is atomic iff Subformulae H = { H }
proof
  thus H is atomic implies Subformulae H = { H }
  proof
    assume H is atomic;
    then H is being_equality or H is being_membership by Def15;
    then H = (Var1 H) '=' Var2 H or H = (Var1 H) 'in' Var2 H by Th36,Th37;
    hence thesis by Th80,Th81;
  end;
  assume
A1: Subformulae H = { H };
A2: now
    assume H = 'not' the_argument_of H;
    then
A3: the_argument_of H is_immediate_constituent_of H by Th52;
    then the_argument_of H is_proper_subformula_of H by Th61;
    then the_argument_of H is_subformula_of H by Def41;
    then
A4: the_argument_of H in Subformulae H by Def42;
    len(the_argument_of H) <> len H by A3,Th60;
    hence contradiction by A1,A4,TARSKI:def 1;
  end;
A5: now
    assume H = (the_left_argument_of H) '&' the_right_argument_of H;
    then
A6: the_left_argument_of H is_immediate_constituent_of H by Th53;
    then the_left_argument_of H is_proper_subformula_of H by Th61;
    then the_left_argument_of H is_subformula_of H by Def41;
    then
A7: the_left_argument_of H in Subformulae H by Def42;
    len(the_left_argument_of H) <> len H by A6,Th60;
    hence contradiction by A1,A7,TARSKI:def 1;
  end;
  assume not H is atomic;
  then H is negative or H is conjunctive or H is universal by Th10;
  then H = 'not' the_argument_of H or H = (the_left_argument_of H) '&'
  the_right_argument_of H or H = All(bound_in H,the_scope_of H) by Def30,Th40
,Th44;
  then
A8: the_scope_of H is_immediate_constituent_of H by A2,A5,Th54;
  then the_scope_of H is_proper_subformula_of H by Th61;
  then the_scope_of H is_subformula_of H by Def41;
  then
A9: the_scope_of H in Subformulae H by Def42;
  len(the_scope_of H) <> len H by A8,Th60;
  hence contradiction by A1,A9,TARSKI:def 1;
end;

theorem
  H is negative implies Subformulae H = Subformulae the_argument_of H \/ { H }
proof
  assume H is negative;
  then H = 'not' the_argument_of H by Def30;
  hence thesis by Th82;
end;

theorem
  H is conjunctive implies Subformulae H = Subformulae
  the_left_argument_of H \/ Subformulae the_right_argument_of H \/ { H }
proof
  assume H is conjunctive;
  then H = (the_left_argument_of H) '&' the_right_argument_of H by Th40;
  hence thesis by Th83;
end;

theorem
  H is universal implies Subformulae H = Subformulae the_scope_of H \/ { H }
proof
  assume H is universal;
  then H = All(bound_in H,the_scope_of H) by Th44;
  hence thesis by Th84;
end;

theorem
  (H is_immediate_constituent_of G or H is_proper_subformula_of G or H
  is_subformula_of G) & G in Subformulae F implies H in Subformulae F
proof
  assume that
A1: H is_immediate_constituent_of G or H is_proper_subformula_of G or H
  is_subformula_of G and
A2: G in Subformulae F;
  H is_proper_subformula_of G or H is_subformula_of G by A1,Th61;
  then
A3: H is_subformula_of G by Def41;
  G is_subformula_of F by A2,Th78;
  then H is_subformula_of F by A3,Th65;
  hence thesis by Def42;
end;

::
::               The Structural Induction Schemes
::

scheme
  ZFInd { P[ZF-formula] } : for H holds P[H]
provided
A1: for H st H is atomic holds P[H] and
A2: for H st H is negative & P[the_argument_of H] holds P[H] and
A3: for H st H is conjunctive & P[the_left_argument_of H] & P[
the_right_argument_of H] holds P[H] and
A4: for H st H is universal & P[the_scope_of H] holds P[H]
proof
  defpred Q[Nat] means for H st len H = $1 holds P[H];
A5: for n being Nat st for k being Nat st k < n holds Q[k] holds Q[n]
  proof
    let n be Nat such that
A6: for k being Nat st k < n for H st len H = k holds P[H];
    let H such that
A7: len H = n;
A8: now
      assume
A9:   H is conjunctive;
      then
A10:  H = (the_left_argument_of H) '&' the_right_argument_of H by Th40;
      then the_right_argument_of H is_immediate_constituent_of H by Th53;
      then len the_right_argument_of H < len H by Th60;
      then
A11:  P[the_right_argument_of H] by A6,A7;
      the_left_argument_of H is_immediate_constituent_of H by A10,Th53;
      then len the_left_argument_of H < len H by Th60;
      then P[the_left_argument_of H] by A6,A7;
      hence thesis by A3,A9,A11;
    end;
A12: now
      assume
A13:  H is universal;
      then H = All(bound_in H,the_scope_of H) by Th44;
      then the_scope_of H is_immediate_constituent_of H by Th54;
      then len the_scope_of H < len H by Th60;
      hence thesis by A4,A6,A7,A13;
    end;
    now
      assume
A14:  H is negative;
      then H = 'not' the_argument_of H by Def30;
      then the_argument_of H is_immediate_constituent_of H by Th52;
      then len the_argument_of H < len H by Th60;
      hence thesis by A2,A6,A7,A14;
    end;
    hence thesis by A1,A8,A12,Th10;
  end;
A15: for n being Nat holds Q[n] from NAT_1:sch 4(A5);
  let H;
  len H = len H;
  hence thesis by A15;
end;

scheme
  ZFCompInd { P[ZF-formula] } : for H holds P[H]
provided
A1: for H st for F st F is_proper_subformula_of H holds P[F] holds P[H]
proof
  defpred Q[Nat] means for H st len H = $1 holds P[H];
A2: for n being Nat st for k be Nat st k < n holds Q[k] holds Q[n]
  proof
    let n be Nat such that
A3: for k being Nat st k < n for H st len H = k holds P[H];
    let H such that
A4: len H = n;
    now
      let F;
      assume F is_proper_subformula_of H;
      then len F < len H by Th62;
      hence P[F] by A3,A4;
    end;
    hence thesis by A1;
  end;
A5: for n being Nat holds Q[n] from NAT_1:sch 4 (A2);
  let H;
  len H = len H;
  hence thesis by A5;
end;