:: The Subformula Tree of a Formula of the First Order Language
::  by Oleg Okhotnikov
::
:: Received October 2, 1995
:: Copyright (c) 1995-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, FINSEQ_1, RELAT_1, TREES_1, XBOOLE_0, ARYTM_3,
      XXREAL_0, ORDINAL4, CARD_1, FUNCT_1, TARSKI, TREES_2, TREES_9, ORDINAL1,
      NAT_1, FINSET_1, QC_LANG1, ZF_LANG, CLASSES2, TREES_4, QC_LANG4;
 notations TARSKI, XBOOLE_0,
      XTUPLE_0, SUBSET_1, CARD_1, NUMBERS, XCMPLX_0, ORDINAL1,
      NAT_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FINSET_1, FINSEQ_1, FINSEQ_4,
      TREES_1, TREES_2, TREES_4, TREES_9, QC_LANG1, QC_LANG2, XXREAL_0;
 constructors BINOP_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_4, TREES_4, TREES_9,
      QC_LANG2, RELSET_1, XTUPLE_0;
 registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XREAL_0, NAT_1,
      FINSEQ_1, TREES_1, TREES_2, TREES_A, TREES_9, CARD_1, RELAT_1, XTUPLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, TREES_2, TREES_4, BINOP_1, XTUPLE_0;
 theorems TARSKI, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, TREES_1, TREES_2, TREES_9,
      GRFUNC_1, QC_LANG1, QC_LANG2, XBOOLE_0, XBOOLE_1, FINSEQ_6, XREAL_1,
      XXREAL_0, ORDINAL1;
 schemes NAT_1, TREES_2, FINSEQ_1, TREES_9;

begin

reserve A for QC-alphabet;
reserve n,k,m for Element of NAT;
reserve F,G,G9,H,H9 for Element of QC-WFF(A);

theorem Th1:
  F is_subformula_of G implies len @ F <= len @ G
proof
  assume
A1: F is_subformula_of G;
  per cases;
  suppose
    F = G;
    hence thesis;
  end;
  suppose
    F <> G;
    then F is_proper_subformula_of G by A1,QC_LANG2:def 21;
    hence thesis by QC_LANG2:54;
  end;
end;

theorem
  F is_subformula_of G & len @ F = len @ G implies F = G
proof
  assume that
A1: F is_subformula_of G and
A2: len @ F = len @ G;
  now
    assume F <> G;
    then F is_proper_subformula_of G by A1,QC_LANG2:def 21;
    hence contradiction by A2,QC_LANG2:54;
  end;
  hence thesis;
end;

definition
  let A;
  let p be Element of QC-WFF(A);
  func list_of_immediate_constituents(p) -> FinSequence of QC-WFF(A) equals
  :Def1:
  <*> QC-WFF(A) if p = VERUM(A) or
  p is atomic, <* the_argument_of p *> if p is
  negative, <* the_left_argument_of p, the_right_argument_of p *> if p is
  conjunctive otherwise <* the_scope_of p *>;
  coherence;
  consistency by QC_LANG1:20;
end;

theorem Th3:
  k in dom list_of_immediate_constituents(F) & G = (
  list_of_immediate_constituents(F)).k implies G is_immediate_constituent_of F
proof
  assume that
A1: k in dom list_of_immediate_constituents(F) and
A2: G = (list_of_immediate_constituents(F)).k;
A3:  list_of_immediate_constituents(F) <> <*>QC-WFF(A) by A1;
A4: F <> VERUM(A) & not F is atomic by Def1,A3;
  per cases by A4,QC_LANG1:9;
  suppose
A5: F is negative;
    then
A6: list_of_immediate_constituents(F) = <* the_argument_of F *> by Def1;
    then k in Seg 1 by A1,FINSEQ_1:def 8;
    then k = 1 by FINSEQ_1:2,TARSKI:def 1;
    then G = the_argument_of F by A2,A6,FINSEQ_1:def 8;
    hence thesis by A5,QC_LANG2:48;
  end;
  suppose
A7: F is universal;
    then
A8: not F is conjunctive by QC_LANG1:20;
    (not F is atomic)& not F is negative by A7,QC_LANG1:20;
    then
A9: list_of_immediate_constituents(F) = <* the_scope_of F *>
      by A8,Def1,A4;
    then k in Seg 1 by A1,FINSEQ_1:def 8;
    then k = 1 by FINSEQ_1:2,TARSKI:def 1;
    then G = the_scope_of F by A2,A9,FINSEQ_1:def 8;
    hence thesis by A7,QC_LANG2:50;
  end;
  suppose
A10: F is conjunctive;
A11: <* the_left_argument_of F, the_right_argument_of F *>.2 =
    the_right_argument_of F by FINSEQ_1:44;
A12: <* the_left_argument_of F, the_right_argument_of F *>.1 =
    the_left_argument_of F by FINSEQ_1:44;
A13: list_of_immediate_constituents(F) = <* the_left_argument_of F,
    the_right_argument_of F *> by A10,Def1;
    len <* the_left_argument_of F, the_right_argument_of F *> = 2 by
FINSEQ_1:44;
    then
A14: k in {1,2} by A1,A13,FINSEQ_1:2,def 3;
    now
      per cases by A14,TARSKI:def 2;
      suppose
        k = 1;
        hence thesis by A2,A10,A13,A12,QC_LANG2:49;
      end;
      suppose
        k = 2;
        hence thesis by A2,A10,A13,A11,QC_LANG2:49;
      end;
    end;
    hence thesis;
  end;
  suppose
A15: F is universal;
    then
A16: not F is conjunctive by QC_LANG1:20;
    (not F is atomic)& not F is negative by A15,QC_LANG1:20;
    then
A17: list_of_immediate_constituents(F) = <* the_scope_of F *>
      by A16,Def1,A4;
    then k in Seg 1 by A1,FINSEQ_1:def 8;
    then k = 1 by FINSEQ_1:2,TARSKI:def 1;
    then G = the_scope_of F by A2,A17,FINSEQ_1:def 8;
    hence thesis by A15,QC_LANG2:50;
  end;
end;

theorem Th4:
  rng list_of_immediate_constituents(F) = { G where G is Element
  of QC-WFF(A) : G is_immediate_constituent_of F }
proof
  thus rng list_of_immediate_constituents(F) c= { G where G is Element of
  QC-WFF(A) : G is_immediate_constituent_of F }
  proof
    let y be set;
    assume
A1: y in rng list_of_immediate_constituents(F);
    rng list_of_immediate_constituents(F) c= QC-WFF(A) by FINSEQ_1:def 4;
    then reconsider G = y as Element of QC-WFF(A) by A1;
    ex x being set st x in dom list_of_immediate_constituents(F) & y = (
    list_of_immediate_constituents(F)).x by A1,FUNCT_1:def 3;
    then G is_immediate_constituent_of F by Th3;
    hence thesis;
  end;
  thus { G where G is Element of QC-WFF(A) :
    G is_immediate_constituent_of F } c=
  rng list_of_immediate_constituents(F)
  proof
    let x be set;
    assume
    x in { G where G is Element of QC-WFF(A) :
    G is_immediate_constituent_of F };
    then consider G such that
A2: x = G and
A3: G is_immediate_constituent_of F;
    ex n st n in dom list_of_immediate_constituents(F) & G = (
    list_of_immediate_constituents(F)).n
    proof
A4:   F <> VERUM(A) by A3,QC_LANG2:41;
      per cases by A3,A4,QC_LANG1:9,QC_LANG2:47;
      suppose
        F is negative;
        then
A5:     list_of_immediate_constituents(F) = <* the_argument_of F *> & G =
        the_argument_of F by A3,Def1,QC_LANG2:48;
        consider n such that
A6:     n = 1;
        dom <* the_argument_of F *> = Seg 1 & <* the_argument_of F *>.n =
        the_argument_of F by A6,FINSEQ_1:def 8;
        hence thesis by A6,A5,FINSEQ_1:3;
      end;
      suppose
A7:     F is conjunctive;
A8:     <* the_left_argument_of F, the_right_argument_of F *>.2 =
        the_right_argument_of F by FINSEQ_1:44;
        len <* the_left_argument_of F, the_right_argument_of F *> = 2 by
FINSEQ_1:44;
        then
A9:     dom <* the_left_argument_of F, the_right_argument_of F *> = Seg 2
        by FINSEQ_1:def 3;
A10:    list_of_immediate_constituents(F) = <* the_left_argument_of F,
        the_right_argument_of F *> by A7,Def1;
A11:    <* the_left_argument_of F, the_right_argument_of F *>.1 =
        the_left_argument_of F by FINSEQ_1:44;
        now
          per cases by A3,A7,QC_LANG2:49;
          suppose
A12:        G = the_left_argument_of F;
            1 in {1,2} by TARSKI:def 2;
            hence thesis by A10,A11,A9,A12,FINSEQ_1:2;
          end;
          suppose
            G = the_right_argument_of F;
            hence thesis by A10,A8,A9,FINSEQ_1:3;

          end;
        end;
        hence thesis;
      end;
      suppose
A13:    F is universal;
        then
A14:    not F is conjunctive by QC_LANG1:20;
        ( not F is atomic)& not F is negative by A13,QC_LANG1:20;
        then
A15:    list_of_immediate_constituents(F) = <* the_scope_of F *> by A14
,Def1,A4;
        consider n such that
A16:    n = 1;
A17:    G = the_scope_of F by A3,A13,QC_LANG2:50;
        dom <* the_scope_of F *> = Seg 1 & <* the_scope_of F *>.n =
        the_scope_of F by A16,FINSEQ_1:def 8;
        hence thesis by A15,A16,A17,FINSEQ_1:3;
      end;
    end;
    hence thesis by A2,FUNCT_1:def 3;
  end;
end;

definition
  let A;
  let p be Element of QC-WFF(A);
  func tree_of_subformulae(p) -> finite DecoratedTree of QC-WFF(A) means
  :Def2:
  it.{} = p & for x being Element of dom it holds succ(it,x) =
  list_of_immediate_constituents(it.x);
  existence
  proof
    deffunc F(Element of QC-WFF(A)) = len @ $1;
    deffunc G(Element of QC-WFF(A)) = list_of_immediate_constituents $1;
    consider W being finite-branching DecoratedTree of QC-WFF(A) such that
A1: W.{} = p & for x being Element of dom W, w being Element of QC-WFF(A)
st w = W.x holds succ(W,x) = G(w)
        from TREES_9:sch 2;
A2: for t,t9 being Element of dom W, d being Element of QC-WFF(A) st t9 in
    succ t & d = W.t9 holds F(d) < F(W.t)
    proof
      let t,t9 be Element of dom W, d be Element of QC-WFF(A) such that
A3:   t9 in succ t and
A4:   d = W.t9;
      consider n such that
A5:   t9 = t^<*n*> and
      t^<*n*> in dom W by A3;
A6:   W.t9 = succ(W,t).(n+1) by A5,TREES_9:40
        .= (list_of_immediate_constituents(W.t)).(n+1) by A1;
      dom list_of_immediate_constituents(W.t) = dom succ(W,t) by A1
        .= dom (t succ) by TREES_9:38;
      then n+1 in dom list_of_immediate_constituents(W.t) by A5,TREES_9:39;
      hence thesis by A4,A6,Th3,QC_LANG2:51;
    end;
    W is finite from TREES_9:sch 3(A2);
    then reconsider W as finite DecoratedTree of QC-WFF(A);
    take W;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let t1, t2 be finite DecoratedTree of QC-WFF(A);
A7: for t1, t2 being finite DecoratedTree of QC-WFF(A) st
  ( t1.{} = p & for
x being Element of dom t1 holds succ(t1,x) = list_of_immediate_constituents(t1.
    x) ) & ( t2.{} = p & for x being Element of dom t2 holds succ(t2,x) =
    list_of_immediate_constituents(t2.x) ) holds t1 c= t2
    proof
      let t1, t2 be finite DecoratedTree of QC-WFF(A);
      assume that
A8:   t1.{} = p and
A9:   for x being Element of dom t1 holds succ(t1,x) =
      list_of_immediate_constituents(t1.x) and
A10:  t2.{} = p and
A11:  for x being Element of dom t2 holds succ(t2,x) =
      list_of_immediate_constituents(t2.x);
      defpred P[set] means $1 in dom t2 & t1.$1 = t2.$1;
A12:  for t being Element of dom t1, n st P[t] & t^<*n*> in dom t1 holds
      P[t^<*n*>]
      proof
        let t be Element of dom t1, n;
        assume that
A13:    P[t] and
A14:    t^<*n*> in dom t1;
        reconsider t9 = t as Element of dom t2 by A13;
A15:    succ(t1,t) = list_of_immediate_constituents(t2.t9) by A9,A13
          .= succ(t2,t9) by A11;
        t^<*n*> in succ t by A14;
        then n < card succ t by TREES_9:7;
        then n < len (t succ) by TREES_9:def 5;
        then n < len succ(t1,t) by TREES_9:28;
        then n < len (t9 succ) by A15,TREES_9:28;
        then n < card succ t9 by TREES_9:def 5;
        then
A16:    t9^<*n*> in succ t9 by TREES_9:7;
        hence t^<*n*> in dom t2;
        thus t1.(t^<*n*>) = succ(t2,t9).(n+1) by A14,A15,TREES_9:40
          .= t2.(t^<*n*>) by A16,TREES_9:40;
      end;
A17:  P[{}] by A8,A10,TREES_1:22;
A18:  for t being Element of dom t1 holds P[t] from TREES_2:sch 1(A17,A12
      );
      then for t being set st t in dom t1 holds t in dom t2;
      then
A19:  dom t1 c= dom t2 by TARSKI:def 3;
      for x being set st x in dom t1 holds t1.x = t2.x by A18;
      hence thesis by A19,GRFUNC_1:2;
    end;
    assume ( t1.{} = p & for x being Element of dom t1 holds succ(t1,x) =
list_of_immediate_constituents(t1.x) )&( t2.{} = p & for x being Element of dom
    t2 holds succ(t2,x) = list_of_immediate_constituents(t2.x) );
    then t1 c= t2 & t2 c= t1 by A7;
    hence thesis by XBOOLE_0:def 10;
  end;
end;

reserve t, t9, t99 for Element of dom tree_of_subformulae(F);

theorem Th5:
  F in rng tree_of_subformulae(F)
proof
  (tree_of_subformulae(F)).{} = F & {} in dom tree_of_subformulae(F) by Def2,
TREES_1:22;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th6:
  t^<*n*> in dom tree_of_subformulae(F) implies ex G st G = (
  tree_of_subformulae(F)).(t^<*n*>) & G is_immediate_constituent_of (
  tree_of_subformulae(F)).t
proof
A1: succ t = {t^<*k*>: t^<*k*> in dom tree_of_subformulae(F)};
  assume t^<*n*> in dom tree_of_subformulae(F);
  then consider t9 such that
A2: t9 = t^<*n*>;
A3: rng list_of_immediate_constituents((tree_of_subformulae(F)).t) = { G1
  where G1 is Element of QC-WFF(A) : G1 is_immediate_constituent_of (
  tree_of_subformulae(F)).t } by Th4;
  consider G such that
A4: G = (tree_of_subformulae(F)).t9;
  t9 in {t^<*k*>: t^<*k*> in dom tree_of_subformulae(F)} by A2;
  then G in rng succ((tree_of_subformulae(F)),t) by A4,A1,TREES_9:41;
  then G in rng list_of_immediate_constituents((tree_of_subformulae(F)).t) by
Def2;
  hence thesis by A2,A4,A3;
end;

theorem Th7:
  H is_immediate_constituent_of (tree_of_subformulae(F)).t iff ex
n st t^<*n*> in dom tree_of_subformulae(F) & H = (tree_of_subformulae(F)).(t^<*
  n*>)
proof
  now
    set G = (tree_of_subformulae(F)).t;
    assume H is_immediate_constituent_of (tree_of_subformulae(F)).t;
    then H in {H1 where H1 is Element of QC-WFF(A) : H1
    is_immediate_constituent_of G };
    then
A1: H in rng list_of_immediate_constituents(G) by Th4;
    succ(tree_of_subformulae(F),t) = list_of_immediate_constituents(G) by Def2;
    then consider t9 such that
A2: H = (tree_of_subformulae(F)).t9 and
A3: t9 in succ t by A1,TREES_9:42;
    ex n st t9 = t^<*n*> & t^<*n*> in dom tree_of_subformulae(F) by A3;
    hence ex n st t^<*n*> in dom tree_of_subformulae(F) & H = (
    tree_of_subformulae(F)).(t^<*n*>) by A2;
  end;
  hence H is_immediate_constituent_of (tree_of_subformulae(F)).t implies ex n
st t^<*n*> in dom tree_of_subformulae(F) & H = (tree_of_subformulae(F)).(t^<*n
  *>);
  given n such that
A4: t^<*n*> in dom tree_of_subformulae(F) and
A5: H = (tree_of_subformulae(F)).(t^<*n*>);
  ex G st G = (tree_of_subformulae(F)).(t^<*n*>) & G
  is_immediate_constituent_of (tree_of_subformulae(F)).t by A4,Th6;
  hence thesis by A5;
end;

theorem Th8:
  G in rng tree_of_subformulae(F) & H is_immediate_constituent_of
  G implies H in rng tree_of_subformulae(F)
proof
  assume that
A1: G in rng tree_of_subformulae(F) and
A2: H is_immediate_constituent_of G;
  consider x being set such that
A3: x in dom tree_of_subformulae(F) and
A4: G = (tree_of_subformulae(F)).x by A1,FUNCT_1:def 3;
  consider t such that
A5: t = x by A3;
  ex n st t^<*n*> in dom tree_of_subformulae(F) & H = ( tree_of_subformulae
  (F)).(t^<*n*>) by A2,A4,A5,Th7;
  hence thesis by FUNCT_1:def 3;
end;

theorem Th9:
  G in rng tree_of_subformulae(F) & H is_subformula_of G implies H
  in rng tree_of_subformulae(F)
proof
  assume that
A1: G in rng tree_of_subformulae(F) and
A2: H is_subformula_of G;
  consider n being Element of NAT, L being FinSequence such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = H and
A6: L.n = G and
A7: for k st 1 <= k & k < n ex H1,G1 being Element of QC-WFF(A) st
   L.k = H1
  & L.(k+1) = G1 & H1 is_immediate_constituent_of G1 by A2,QC_LANG2:def 20;
  defpred P[Nat] means ex H9 st H9 = L.($1+1) & ($1+1) in dom L & H9 in rng
  tree_of_subformulae(F);
A8: for k being Nat st k <> 0 & P[k] ex m being Nat st m < k & P[m]
  proof
A9: Seg n = dom L by A4,FINSEQ_1:def 3;
    let k be Nat;
    assume that
A10: k <> 0 and
A11: P[k];
    consider m being Nat such that
A12: m+1 = k by A10,NAT_1:6;
    0 < k by A10,NAT_1:3;
    then
A13: 0+1 <= k by NAT_1:13;
    Seg len L = dom L by FINSEQ_1:def 3;
    then
A14: k+1 <= n by A4,A11,FINSEQ_1:1;
    then k in NAT & k < n by NAT_1:13,ORDINAL1:def 12;
    then
A15: ex H1,G1 being Element of QC-WFF(A) st L.k = H1 & L.(k+1) = G1 & H1
    is_immediate_constituent_of G1 by A7,A13;
    k <= n by A14,NAT_1:13;
    then
A16: k in dom L by A13,A9,FINSEQ_1:1;
    m < k by A12,NAT_1:13;
    hence thesis by A11,A12,A15,A16,Th8;
  end;
A17: ex k being Nat st P[k]
  proof
    0 <> n by A3;
    then
A18: ex k being Nat st k+1 = n by NAT_1:6;
    Seg n = dom L by A4,FINSEQ_1:def 3;
    hence thesis by A1,A6,A18,FINSEQ_1:3;
  end;
  P[0] from NAT_1:sch 7(A17,A8);
  hence thesis by A5;
end;

theorem Th10:
  G in rng tree_of_subformulae(F) iff G is_subformula_of F
proof
  now
    set T = dom tree_of_subformulae(F);
    defpred P[set] means ex H st (tree_of_subformulae(F)).$1 = H & H
    is_subformula_of F;
    assume G in rng tree_of_subformulae(F);
    then consider t being set such that
A1: t in dom tree_of_subformulae(F) and
A2: (tree_of_subformulae(F)).t = G by FUNCT_1:def 3;
    reconsider t as Element of T by A1;
A3: for t being Element of T, n st P[t] & t^<*n*> in T holds P[t^<*n*>]
    proof
      let t be Element of T, n;
      assume that
A4:   P[t] and
A5:   t^<*n*> in T;
      (tree_of_subformulae(F)).(t^<*n*>) is Element of QC-WFF(A)
         by A5,FUNCT_1:102;
      then consider H9 such that
A6:   (tree_of_subformulae(F)).(t^<*n*>) = H9;
      consider H such that
A7:   (tree_of_subformulae(F)).t = H and
A8:   H is_subformula_of F by A4;
      ex G9 st G9 = (tree_of_subformulae(F)).(t^<*n*>) & G9
      is_immediate_constituent_of (tree_of_subformulae(F)).t by A5,Th6;
      then H9 is_subformula_of H by A7,A6,QC_LANG2:52;
      hence thesis by A8,A6,QC_LANG2:57;
    end;
A9: P[{}]
    proof
      take F;
      thus thesis by Def2;
    end;
    for t being Element of T holds P[t] from TREES_2:sch 1(A9,A3);
    then ex H st (tree_of_subformulae(F)).t = H & H is_subformula_of F;
    hence G is_subformula_of F by A2;
  end;
  hence G in rng tree_of_subformulae(F) implies G is_subformula_of F;
  assume G is_subformula_of F;
  hence thesis by Th5,Th9;
end;

theorem
  rng tree_of_subformulae(F) = Subformulae(F)
proof
  thus rng tree_of_subformulae(F) c= Subformulae(F)
  proof
    let y be set;
    assume
A1: y in rng tree_of_subformulae(F);
    then y is Element of QC-WFF(A) by RELAT_1:167;
    then consider G such that
A2: G = y;
    G is_subformula_of F by A1,A2,Th10;
    hence thesis by A2,QC_LANG2:def 22;
  end;
  thus Subformulae(F) c= rng tree_of_subformulae(F)
  proof
    let y be set;
    assume y in Subformulae(F);
    then ex G st G = y & G is_subformula_of F by QC_LANG2:def 22;
    hence thesis by Th10;
  end;
end;

theorem
  t9 in succ t implies (tree_of_subformulae(F)).t9
  is_immediate_constituent_of (tree_of_subformulae(F)).t
proof
  assume t9 in succ t;
  then ex n st t9 = t^<*n*> & t^<*n*> in dom tree_of_subformulae(F);
  hence thesis by Th7;
end;

reserve x for set;

theorem Th13:
  t is_a_prefix_of t9 implies (tree_of_subformulae(F)).t9
  is_subformula_of (tree_of_subformulae(F)).t
proof
  assume t is_a_prefix_of t9;
  then consider r being FinSequence such that
A1: t9 = t^r by TREES_1:1;
  reconsider r as FinSequence of NAT by A1,FINSEQ_1:36;
  consider n such that
A2: n = len r;
  defpred P[set,set] means ex G being QC-formula of A,
  m,k1 being Nat, r1 being
  FinSequence st G = $2 & m = $1 & m+k1 = n+1 & r1 = r|Seg k1 & G = (
  tree_of_subformulae(F)).(t^r1);
A3: for k be Nat st k in Seg(n+1) ex x st P[k,x]
  proof
    let k be Nat;
    assume k in Seg(n+1);
    then k <= n+1 by FINSEQ_1:1;
    then consider k1 being Nat such that
A4: k+k1 = n+1 by NAT_1:10;
    reconsider k1 as Element of NAT by ORDINAL1:def 12;
    r|Seg k1 is FinSequence by FINSEQ_1:15;
    then consider r1 being FinSequence such that
A5: r1 = r|Seg k1;
    t^r1 in dom tree_of_subformulae(F)
    proof
      ex q being FinSequence st q = r|Seg k1 & q is_a_prefix_of r
       by TREES_9:32;
      hence thesis by A1,A5,FINSEQ_6:13,TREES_1:20;
    end;
    then reconsider t1 = t^r1 as Element of dom tree_of_subformulae(F);
    consider G being QC-formula of A such that
A6: G = (tree_of_subformulae(F)).t1;
    take G,G,k,k1,r1;
    thus thesis by A4,A5,A6;
  end;
  ex L being FinSequence st dom L = Seg(n+1) & for k be Nat st k in Seg(n
  +1) holds P[k,L.k] from FINSEQ_1:sch 1(A3);
  then consider L being FinSequence such that
A7: dom L = Seg (n+1) and
A8: for k be Nat st k in Seg (n+1) holds ex G being QC-formula of A, m,k1
being Nat, r1 being FinSequence st G = L.k & m = k & m+k1 = n+1 & r1 = r|Seg k1
  & G = (tree_of_subformulae(F)).(t^r1);
A9: len L = n+1 by A7,FINSEQ_1:def 3;
A10: for k st 1 <= k & k <= n+1 ex G being QC-formula of A,
k1 being Nat, r1
  being FinSequence st G = L.k & k+k1 = n+1 & r1 = r|Seg k1 & G = (
  tree_of_subformulae(F)).(t^r1)
  proof
    let k;
    assume 1 <= k & k <= n+1;
    then k in Seg (n+1) by FINSEQ_1:1;
    then
    ex G being QC-formula of A, m,k1 being Nat,
     r1 being FinSequence st G = L.k
& m = k & m+k1 = n+1 & r1 = r|Seg k1 & G = ( tree_of_subformulae(F)).(t^r1) by
A8;
    hence thesis;
  end;
A11: for k st 1 <= k & k < n+1 ex H1,G1 being Element of QC-WFF(A)
  st L.k = H1
  & L.(k+1) = G1 & H1 is_immediate_constituent_of G1
  proof
    let k;
    assume that
A12: 1 <= k and
A13: k < n+1;
    consider H1 being QC-formula of A, k1 being Nat,
     r1 being FinSequence such that
A14: H1 = L.k and
A15: k+k1 = n+1 and
A16: r1 = r|Seg k1 and
A17: H1 = (tree_of_subformulae(F)).(t^r1) by A10,A12,A13;
    1 <= k+1 & k+1 <= n+1 by A12,A13,NAT_1:13;
    then consider
    G1 being QC-formula of A,
      k2 being Nat, r2 being FinSequence such that
A18: G1 = L.(k+1) and
A19: (k+1)+k2 = n+1 and
A20: r2 = r|Seg k2 and
A21: G1 = (tree_of_subformulae(F)).(t^r2) by A10;
    reconsider k1,k2 as Element of NAT by ORDINAL1:def 12;
    k1+1 <= n+1 by A12,A15,XREAL_1:6;
    then k2+1 <= len r by A2,A15,A19,XREAL_1:6;
    then consider m such that
A22: r1 = r2^<*m*> by A15,A16,A19,A20,TREES_9:33;
    t^r2 in dom tree_of_subformulae(F)
    proof
      ex q being FinSequence st q = r|Seg k2 & q is_a_prefix_of r
       by TREES_9:32;
      hence thesis by A1,A20,FINSEQ_6:13,TREES_1:20;
    end;
    then reconsider t2 = t^r2 as Element of dom tree_of_subformulae(F);
A23: t2^<*m*> = t^r1 by A22,FINSEQ_1:32;
    t2^<*m*> in dom tree_of_subformulae(F)
    proof
      ex q being FinSequence st q = r|Seg k1 & q is_a_prefix_of r
       by TREES_9:32;
      hence thesis by A1,A16,A23,FINSEQ_6:13,TREES_1:20;
    end;
    then H1 is_immediate_constituent_of G1 by A17,A21,A23,Th7;
    hence thesis by A14,A18;
  end;
  0 < n+1 by NAT_1:3;
  then
A24: 0+1 <= n+1 by NAT_1:13;
  then consider
  G being QC-formula of A, k1 being Nat, r1 being FinSequence such that
A25: G = L.1 and
A26: 1+k1 = n+1 and
A27: r1 = r|Seg k1 and
A28: G = (tree_of_subformulae(F)).(t^r1) by A10;
A29: L.(n+1) = (tree_of_subformulae(F)).t
  proof
    consider G being QC-formula of A,
    k1 being Nat, r1 being FinSequence such that
A30: G = L.(n+1) and
A31: (n+1)+k1 = n+1 & r1 = r|Seg k1 and
A32: G = (tree_of_subformulae(F)).(t^r1) by A24,A10;
    r1 = {} by A31;
    hence thesis by A30,A32,FINSEQ_1:34;
  end;
  dom r = Seg k1 by A2,A26,FINSEQ_1:def 3;
  then t9 = t^r1 by A1,A27,RELAT_1:69;
  hence thesis by A24,A9,A25,A28,A29,A11,QC_LANG2:def 20;
end;

theorem Th14:
  t is_a_proper_prefix_of t9 implies len @((tree_of_subformulae(F)
  ).t9) < len @((tree_of_subformulae(F)).t)
proof
  set G = (tree_of_subformulae(F)).t;
  set H = (tree_of_subformulae(F)).t9;
  assume
A1: t is_a_proper_prefix_of t9;
  then
A2: t is_a_prefix_of t9 by XBOOLE_0:def 8;
A3: now
    consider r being FinSequence such that
A4: t9 = t^r by A2,TREES_1:1;
    reconsider r as FinSequence of NAT by A4,FINSEQ_1:36;
A5: 1 <= len r
    proof
      reconsider t1 = {} as Element of dom tree_of_subformulae(F) by TREES_1:22
;
      r <> {} & t1 is_a_prefix_of r by A1,A4,FINSEQ_1:34,XBOOLE_1:2;
      then
A6:   t1 is_a_proper_prefix_of r by XBOOLE_0:def 8;
      len t1 = 0;
      then 0 < len r by A6,TREES_1:6;
      then 0+1 <= len r by NAT_1:13;
      hence thesis;
    end;
    defpred P[set,set] means ex t1 being Element of dom tree_of_subformulae(F)
, r1 being FinSequence, m being Nat st m = $1 & r1 = r|Seg m & t1 = t^r1 & $2 =
    (tree_of_subformulae(F)).t1;
A7: for k be Nat st k in Seg len r ex x st P[k,x]
    proof
      let k be Nat such that
A8:   k in Seg len r;
      r|Seg k is FinSequence by FINSEQ_1:15;
      then consider r1 being FinSequence such that
A9:   r1 = r|Seg k;
      r1 is_a_prefix_of r by A8,A9,TREES_1:def 1;
      then t^r1 in dom tree_of_subformulae(F) by A4,FINSEQ_6:13,TREES_1:20;
      then consider t1 being Element of dom tree_of_subformulae(F) such that
A10:  t1 = t^r1;
      ex x st x = (tree_of_subformulae(F)).t1;
      hence thesis by A9,A10;
    end;
    ex L being FinSequence st dom L = Seg len r & for k be Nat st k in
    Seg len r holds P[k,L.k] from FINSEQ_1:sch 1(A7);
    then consider L being FinSequence such that
    dom L = Seg len r and
A11: for k be Nat st k in Seg len r holds ex t1 being Element of dom
tree_of_subformulae(F), r1 being FinSequence, m being Nat st m = k & r1 = r|Seg
    m & t1 = t^r1 & L.k = (tree_of_subformulae(F)).t1;
    for k st 1 <= k & k <= len r holds ex t1 being Element of dom
tree_of_subformulae(F), r1 being FinSequence st r1 = r|Seg k & t1 = t^r1 & L.k
    = (tree_of_subformulae(F)).t1
    proof
      let k;
      assume 1 <= k & k <= len r;
      then k in Seg len r by FINSEQ_1:1;
      then ex t1 being Element of dom tree_of_subformulae(F), r1 being
      FinSequence, m being Nat st m = k & r1 = r|Seg m & t1 = t^r1 & L.k = (
      tree_of_subformulae(F)).t1 by A11;
      hence thesis;
    end;
    then consider t1 being Element of dom tree_of_subformulae(F), r1 being
    FinSequence such that
A12: r1 = r|Seg 1 and
A13: t1 = t^r1 and
    L.1 = (tree_of_subformulae(F)).t1 by A5;
    set H1 = (tree_of_subformulae(F)).t1;
A14: H1 is_immediate_constituent_of G
    proof
      ex m being Element of NAT st r1 = <*m*> by A5,A12,TREES_9:34;
      hence thesis by A13,Th7;
    end;
    r1 is_a_prefix_of r by A12,TREES_1:def 1;
    then t1 is_a_prefix_of t9 by A4,A13,FINSEQ_6:13;
    then
A15: len @ H <= len @ H1 by Th1,Th13;
    assume len @ H = len @ G;
    hence contradiction by A15,A14,QC_LANG2:51;
  end;
  len @ H <= len @ G by A2,Th1,Th13;
  hence thesis by A3,XXREAL_0:1;
end;

theorem Th15:
  t is_a_proper_prefix_of t9 implies (tree_of_subformulae(F)).t9
  <> (tree_of_subformulae(F)).t
proof
  set G = (tree_of_subformulae(F)).t;
  set H = (tree_of_subformulae(F)).t9;
  assume t is_a_proper_prefix_of t9;
  then len @H < len @G by Th14;
  hence thesis;
end;

theorem Th16:
  t is_a_proper_prefix_of t9 implies (tree_of_subformulae(F)).t9
  is_proper_subformula_of (tree_of_subformulae(F)).t
proof
  set G = (tree_of_subformulae(F)).t;
  set H = (tree_of_subformulae(F)).t9;
  assume
A1: t is_a_proper_prefix_of t9;
  then t is_a_prefix_of t9 by XBOOLE_0:def 8;
  then
A2: H is_subformula_of G by Th13;
  H <> G by A1,Th15;
  hence thesis by A2,QC_LANG2:def 21;
end;

theorem
  (tree_of_subformulae(F)).t = F iff t = {}
proof
  now
    reconsider t1 = {} as Element of dom tree_of_subformulae(F) by TREES_1:22;
    assume
A1: (tree_of_subformulae(F)).t = F;
A2: t1 is_a_prefix_of t by XBOOLE_1:2;
    assume t <> {};
    then t1 is_a_proper_prefix_of t by A2,XBOOLE_0:def 8;
    then (tree_of_subformulae(F)).t is_proper_subformula_of (
    tree_of_subformulae(F)).t1 by Th16;
    hence contradiction by A1,Def2;
  end;
  hence (tree_of_subformulae(F)).t = F implies t = {};
  assume t = {};
  hence thesis by Def2;
end;

theorem Th18:
  t <> t9 & (tree_of_subformulae(F)).t = (tree_of_subformulae(F)).
  t9 implies not t,t9 are_c=-comparable
proof
  assume that
A1: t <> t9 and
A2: (tree_of_subformulae(F)).t = (tree_of_subformulae(F)).t9;
  assume
A3: t,t9 are_c=-comparable;
  per cases by A3,XBOOLE_0:def 9;
  suppose
    t is_a_prefix_of t9;
    then t is_a_proper_prefix_of t9 by A1,XBOOLE_0:def 8;
    hence contradiction by A2,Th16;
  end;
  suppose
    t9 is_a_prefix_of t;
    then t9 is_a_proper_prefix_of t by A1,XBOOLE_0:def 8;
    hence contradiction by A2,Th16;
  end;
end;

definition
  let A;
  let F, G be Element of QC-WFF(A);
  func F-entry_points_in_subformula_tree_of G -> AntiChain_of_Prefixes of dom
  tree_of_subformulae(F) means
  :Def3:
  for t being Element of dom
  tree_of_subformulae(F) holds t in it iff (tree_of_subformulae(F)).t = G;
  existence
  proof
    consider X being set such that
A1: X = { t where t is Element of dom tree_of_subformulae(F) : (
    tree_of_subformulae(F)).t = G };
A2: X is AntiChain_of_Prefixes of dom tree_of_subformulae(F)
    proof
A3:   for p1,p2 being FinSequence st p1 in X & p2 in X & p1 <> p2 holds
      not p1,p2 are_c=-comparable
      proof
        let p1,p2 be FinSequence;
        assume that
A4:     p1 in X & p2 in X and
A5:     p1 <> p2;
        (ex t1 being Element of dom tree_of_subformulae(F) st t1 = p1 & (
        tree_of_subformulae(F)).t1 = G )& ex t2 being Element of dom
tree_of_subformulae(F) st t2 = p2 & (tree_of_subformulae(F)).t2 = G by A1,A4;
        hence thesis by A5,Th18;
      end;
      for x being set st x in X holds x is FinSequence
      proof
        let x be set;
        assume x in X;
        then ex t being Element of dom tree_of_subformulae(F) st t = x & (
        tree_of_subformulae(F)).t = G by A1;
        hence thesis;
      end;
      then reconsider X as AntiChain_of_Prefixes by A3,TREES_1:def 10;
      X c= dom tree_of_subformulae(F)
      proof
        let x be set;
        assume x in X;
        then ex t being Element of dom tree_of_subformulae(F) st t = x & (
        tree_of_subformulae(F)).t = G by A1;
        hence thesis;
      end;
      hence thesis by TREES_1:def 11;
    end;
    for t being Element of dom tree_of_subformulae(F) holds t in X iff (
    tree_of_subformulae(F)).t = G
    proof
      let t be Element of dom tree_of_subformulae(F);
      thus t in X iff (tree_of_subformulae(F)).t = G
      proof
        now
          assume t in X;
          then ex t9 being Element of dom tree_of_subformulae(F) st t9 = t & (
          tree_of_subformulae(F)).t9 = G by A1;
          hence (tree_of_subformulae(F)).t = G;
        end;
        hence t in X implies (tree_of_subformulae(F)).t = G;
        assume (tree_of_subformulae(F)).t = G;
        hence thesis by A1;
      end;
    end;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let P1,P2 be AntiChain_of_Prefixes of dom tree_of_subformulae(F);
    assume
A6: for t being Element of dom tree_of_subformulae(F) holds t in P1
    iff (tree_of_subformulae(F)).t = G;
    assume
A7: for t being Element of dom tree_of_subformulae(F) holds t in P2
    iff (tree_of_subformulae(F)).t = G;
    thus P1 c= P2
    proof
      let x be set such that
A8:   x in P1;
      P1 c= dom tree_of_subformulae(F) by TREES_1:def 11;
      then reconsider t = x as Element of dom tree_of_subformulae(F) by A8;
      (tree_of_subformulae(F)).t = G by A6,A8;
      hence thesis by A7;
    end;
    thus P2 c= P1
    proof
      let x be set such that
A9:   x in P2;
      P2 c= dom tree_of_subformulae(F) by TREES_1:def 11;
      then reconsider t = x as Element of dom tree_of_subformulae(F) by A9;
      (tree_of_subformulae(F)).t = G by A7,A9;
      hence thesis by A6;
    end;
  end;
end;

theorem Th19:
  F-entry_points_in_subformula_tree_of G = { t where t is Element
  of dom tree_of_subformulae(F) : (tree_of_subformulae(F)).t = G }
proof
  thus F-entry_points_in_subformula_tree_of G c= { t where t is Element of dom
  tree_of_subformulae(F) : (tree_of_subformulae(F)).t = G }
  proof
    let x be set;
    assume
A1: x in F-entry_points_in_subformula_tree_of G;
    F-entry_points_in_subformula_tree_of G c= dom tree_of_subformulae(F)
    by TREES_1:def 11;
    then reconsider t9 = x as Element of dom tree_of_subformulae(F) by A1;
    (tree_of_subformulae(F)).t9 = G by A1,Def3;
    hence thesis;
  end;
  thus { t where t is Element of dom tree_of_subformulae(F) : (
  tree_of_subformulae(F)).t = G } c= F-entry_points_in_subformula_tree_of G
  proof
    let x be set;
    assume x in { t where t is Element of dom tree_of_subformulae(F) : (
    tree_of_subformulae(F)).t = G };
    then ex t9 st t9 = x & (tree_of_subformulae(F)).t9 = G;
    hence thesis by Def3;
  end;
end;

theorem Th20:
  G is_subformula_of F iff F-entry_points_in_subformula_tree_of G <> {}
proof
  now
    assume G is_subformula_of F;
    then G in rng tree_of_subformulae(F) by Th10;
    then ex x being set st x in dom tree_of_subformulae(F) & G = (
    tree_of_subformulae(F)).x by FUNCT_1:def 3;
    hence F-entry_points_in_subformula_tree_of G <> {} by Def3;
  end;
  hence G is_subformula_of F implies F-entry_points_in_subformula_tree_of G <>
  {};
  assume F-entry_points_in_subformula_tree_of G <> {};
  then consider x being set such that
A1: x in F-entry_points_in_subformula_tree_of G by XBOOLE_0:def 1;
  x in { t where t is Element of dom tree_of_subformulae(F) : (
  tree_of_subformulae(F)).t = G } by A1,Th19;
  then ex t st x = t & (tree_of_subformulae(F)).t = G;
  then G in rng tree_of_subformulae(F) by FUNCT_1:def 3;
  hence thesis by Th10;
end;

theorem Th21:
  t9 = t^<*m*> & (tree_of_subformulae(F)).t is negative implies (
tree_of_subformulae(F)).t9 = the_argument_of (tree_of_subformulae(F)).t & m = 0
proof
  set G = (tree_of_subformulae(F)).t;
  set H = (tree_of_subformulae(F)).t9;
  assume that
A1: t9 = t^<*m*> and
A2: G is negative;
A3: dom <* the_argument_of G *> = Seg 1 by FINSEQ_1:def 8;
A4: succ(tree_of_subformulae(F),t) = list_of_immediate_constituents(G) & ex
  q being Element of dom tree_of_subformulae(F) st q = t & succ(
  tree_of_subformulae(F),t) = tree_of_subformulae(F)*(q succ) by Def2,
TREES_9:def 6;
  list_of_immediate_constituents(G) = <* the_argument_of G *> by A2,Def1;
  then dom <* the_argument_of G *> = dom (t succ) by A4,TREES_9:37;
  then m+1 in dom <* the_argument_of G *> by A1,TREES_9:39;
  then
A5: m+1 = 0+1 by A3,FINSEQ_1:2,TARSKI:def 1;
  H is_immediate_constituent_of G by A1,Th7;
  hence thesis by A2,A5,QC_LANG2:48;

end;

theorem Th22:
  t9 = t^<*m*> & (tree_of_subformulae(F)).t is conjunctive implies
(tree_of_subformulae(F)).t9 = the_left_argument_of (tree_of_subformulae(F)).t &
  m = 0 or (tree_of_subformulae(F)).t9 = the_right_argument_of (
  tree_of_subformulae(F)).t & m = 1
proof
  set G = (tree_of_subformulae(F)).t;
  set H = (tree_of_subformulae(F)).t9;
  assume that
A1: t9 = t^<*m*> and
A2: G is conjunctive;
A3: list_of_immediate_constituents(G) = <* the_left_argument_of G,
  the_right_argument_of G *> by A2,Def1;
  len <* the_left_argument_of G, the_right_argument_of G *> = 2 by FINSEQ_1:44;
  then
A4: dom <* the_left_argument_of G, the_right_argument_of G *> = Seg 2 by
FINSEQ_1:def 3;
A5: succ(tree_of_subformulae(F),t) = list_of_immediate_constituents(G) by Def2;
  ex q being Element of dom tree_of_subformulae(F) st q = t & succ(
  tree_of_subformulae(F),t) = tree_of_subformulae(F)*(q succ) by TREES_9:def 6;
  then
  dom <* the_left_argument_of G, the_right_argument_of G *> = dom (t succ)
  by A5,A3,TREES_9:37;
  then
  m+1 in dom <* the_left_argument_of G, the_right_argument_of G *> by A1,
TREES_9:39;
  then
A6: m+1 = 0+1 or m+1 = 1+1 by A4,FINSEQ_1:2,TARSKI:def 2;
  per cases by A6;
  suppose
A7: m = 0;
    H = succ(tree_of_subformulae(F),t).(m+1) by A1,TREES_9:40
      .= the_left_argument_of G by A5,A3,A7,FINSEQ_1:44;
    hence thesis by A7;
  end;
  suppose
A8: m = 1;
    H = succ(tree_of_subformulae(F),t).(m+1) by A1,TREES_9:40
      .= the_right_argument_of G by A5,A3,A8,FINSEQ_1:44;
    hence thesis by A8;
  end;
end;

theorem Th23:
  t9 = t^<*m*> & (tree_of_subformulae(F)).t is universal implies (
  tree_of_subformulae(F)).t9 = the_scope_of (tree_of_subformulae(F)).t & m = 0
proof
  set G = (tree_of_subformulae(F)).t;
  set H = (tree_of_subformulae(F)).t9;
  assume that
A1: t9 = t^<*m*> and
A2: G is universal;
A3: dom <* the_scope_of G *> = Seg 1 by FINSEQ_1:def 8;
A4: succ(tree_of_subformulae(F),t) = list_of_immediate_constituents(G) & ex
  q being Element of dom tree_of_subformulae(F) st q = t & succ(
  tree_of_subformulae(F),t) = tree_of_subformulae(F)*(q succ) by Def2,
TREES_9:def 6;
   VERUM(A) is not universal by QC_LANG1:20; then
A5: G <> VERUM(A) by A2;
  G is non atomic non negative non conjunctive by A2,QC_LANG1:20;
  then list_of_immediate_constituents(G) = <* the_scope_of G *> by Def1,A5;
  then dom <* the_scope_of G *> = dom (t succ) by A4,TREES_9:37;
  then m+1 in dom <* the_scope_of G *> by A1,TREES_9:39;
  then
A6: m+1 = 0+1 by A3,FINSEQ_1:2,TARSKI:def 1;
  H is_immediate_constituent_of G by A1,Th7;
  hence thesis by A2,A6,QC_LANG2:50;
end;

theorem Th24:
  (tree_of_subformulae(F)).t is negative implies t^<*0*> in dom
tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*0*>) = the_argument_of (
  tree_of_subformulae(F)).t
proof

  set G = (tree_of_subformulae(F)).t;
  consider H such that
A1: H = the_argument_of G;
  assume
A2: G is negative;
  then H is_immediate_constituent_of G by A1,QC_LANG2:48;
  then consider m such that
A3: t^<*m*> in dom tree_of_subformulae(F) and
  H = (tree_of_subformulae(F)).(t^<*m*>) by Th7;
  m = 0 by A2,A3,Th21;
  hence thesis by A2,A3,Th21;
end;

reserve x,y for set;

Lm1: dom <* x, y *> = Seg 2
proof
  thus dom <* x, y *> = Seg len <* x, y *> by FINSEQ_1:def 3
    .= Seg 2 by FINSEQ_1:44;
end;

theorem Th25:
  (tree_of_subformulae(F)).t is conjunctive implies t^<*0*> in dom
  tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*0*>) =
  the_left_argument_of (tree_of_subformulae(F)).t & t^<*1*> in dom
  tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*1*>) =
  the_right_argument_of (tree_of_subformulae(F)).t
proof
  set G = (tree_of_subformulae(F)).t;
  assume
A1: G is conjunctive;
  (tree_of_subformulae(F))*(t succ) = (succ(tree_of_subformulae(F),t))
  proof
    ex q being Element of dom tree_of_subformulae(F) st q = t & succ(
tree_of_subformulae(F),t) = (tree_of_subformulae(F))*(q succ) by TREES_9:def 6;
    hence thesis;
  end;
  then
A2: dom (t succ) = dom (succ(tree_of_subformulae(F),t)) by TREES_9:37
    .= dom (list_of_immediate_constituents(G)) by Def2
    .= dom <* the_left_argument_of G, the_right_argument_of G *> by A1,Def1
    .= {1,2} by Lm1,FINSEQ_1:2;
A3: 0+1 in {1,2} by TARSKI:def 2;
  then t^<*0*> in dom tree_of_subformulae(F) by A2,TREES_9:39;
  then
  (tree_of_subformulae(F)).(t^<*0*>) = (succ(tree_of_subformulae(F),t)).(0
  +1) by TREES_9:40
    .= (list_of_immediate_constituents(G)).1 by Def2
    .= <* the_left_argument_of G, the_right_argument_of G *>.1 by A1,Def1
    .= the_left_argument_of G by FINSEQ_1:44;
  hence
  t^<*0*> in dom tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*0
  *>) = the_left_argument_of (tree_of_subformulae(F)).t by A2,A3,TREES_9:39;
A4: 1+1 in {1,2} by TARSKI:def 2;
  then t^<*1*> in dom tree_of_subformulae(F) by A2,TREES_9:39;
  then
  (tree_of_subformulae(F)).(t^<*1*>) = (succ(tree_of_subformulae(F),t)).(
  1+1) by TREES_9:40
    .= (list_of_immediate_constituents(G)).2 by Def2
    .= <* the_left_argument_of G, the_right_argument_of G *>.2 by A1,Def1
    .= the_right_argument_of G by FINSEQ_1:44;
  hence thesis by A2,A4,TREES_9:39;
end;

theorem Th26:
  (tree_of_subformulae(F)).t is universal implies t^<*0*> in dom
  tree_of_subformulae(F) & (tree_of_subformulae(F)).(t^<*0*>) = the_scope_of (
  tree_of_subformulae(F)).t
proof

  set G = (tree_of_subformulae(F)).t;
  consider H such that
A1: H = the_scope_of G;
  assume
A2: G is universal;
  then H is_immediate_constituent_of G by A1,QC_LANG2:50;
  then consider m such that
A3: t^<*m*> in dom tree_of_subformulae(F) and
  H = (tree_of_subformulae(F)).(t^<*m*>) by Th7;
  m = 0 by A2,A3,Th23;
  hence thesis by A2,A3,Th23;
end;

reserve t for Element of dom tree_of_subformulae(F),
  s for Element of dom tree_of_subformulae(G);

theorem Th27:
  t in F-entry_points_in_subformula_tree_of G & s in G
  -entry_points_in_subformula_tree_of H implies t^s in F
  -entry_points_in_subformula_tree_of H
proof
  defpred P[Element of NAT] means for F,G,H,t,s holds G = (tree_of_subformulae
  (F)).t & H = (tree_of_subformulae(G)).s & len s = $1 implies t^s in F
  -entry_points_in_subformula_tree_of H;
A1: for k st P[k] holds P[k + 1]
  proof
    let k such that
A2: P[k];
    thus P[k + 1]
    proof
A3:   1 in {1} by TARSKI:def 1;
      let F,G,H,t,s;
      assume that
A4:   G = (tree_of_subformulae(F)).t and
A5:   H = (tree_of_subformulae(G)).s and
A6:   len s = k+1;
      consider v being FinSequence, x being set such that
A7:   s = v^<*x*> and
A8:   len v = k by A6,TREES_2:3;
      reconsider u = <*x*> as FinSequence of NAT by A7,FINSEQ_1:36;
A9:   rng u c= NAT by FINSEQ_1:def 4;
      dom u = Seg 1 & u.1 = x by FINSEQ_1:def 8;
      then x in rng u by A3,FINSEQ_1:2,FUNCT_1:def 3;
      then reconsider m = x as Element of NAT by A9;
      reconsider v as FinSequence of NAT by A7,FINSEQ_1:36;
      reconsider s9 = v as Element of dom tree_of_subformulae(G) by A7,
TREES_1:21;
      consider H9 such that
A10:  H9 = (tree_of_subformulae(G)).s9;
A11:  t^s9 in F-entry_points_in_subformula_tree_of H9 by A2,A4,A8,A10;
      F-entry_points_in_subformula_tree_of H9 c= dom tree_of_subformulae(
      F) by TREES_1:def 11;
      then consider t9 being Element of dom tree_of_subformulae(F) such that
A12:  t9 = t^s9 by A11;
A13:  H9 = (tree_of_subformulae(F)).t9 by A11,A12,Def3;
A14:  s = s9^<*m*> by A7;
      then
A15:  H is_immediate_constituent_of H9 by A5,A10,Th7;
A16:  H = (tree_of_subformulae(F)).(t9^<*m*>) & t9^<*m*> in dom
      tree_of_subformulae(F)
      proof
A17:    H9 <> VERUM(A) by A15,QC_LANG2:41;
        now
          per cases by A15,A17,QC_LANG1:9,QC_LANG2:47;
          suppose
A18:        H9 is negative;
            then H = the_argument_of H9 & m = 0 by A5,A14,A10,Th21;
            hence thesis by A13,A18,Th24;
          end;
          suppose
A19:        H9 is conjunctive;
            then H = the_left_argument_of H9 & m = 0 or H =
            the_right_argument_of H9 & m = 1 by A5,A14,A10,Th22;
            hence thesis by A13,A19,Th25;
          end;
          suppose
A20:        H9 is universal;
            then H = the_scope_of H9 & m = 0 by A5,A14,A10,Th23;
            hence thesis by A13,A20,Th26;
          end;
        end;
        hence thesis;
      end;
      t^s = t9^<*m*> by A7,A12,FINSEQ_1:32;
      hence thesis by A16,Def3;
    end;
  end;
A21: P[0]
  proof
    let F,G,H,t,s;
    assume that
A22: G = (tree_of_subformulae(F)).t and
A23: H = (tree_of_subformulae(G)).s and
A24: len s = 0;
A25: s = {} by A24;
    then
A26: t^s = t by FINSEQ_1:34;
    H = G by A23,A25,Def2;
    hence thesis by A22,A26,Def3;
  end;
  for k holds P[k] from NAT_1:sch 1(A21,A1);
  then
A27: G = (tree_of_subformulae(F)).t & H = (tree_of_subformulae(G)).s & len s
  = len s implies t^s in F-entry_points_in_subformula_tree_of H;
  assume t in F-entry_points_in_subformula_tree_of G & s in G
  -entry_points_in_subformula_tree_of H;
  hence thesis by A27,Def3;
end;

reserve t for Element of dom tree_of_subformulae(F),
  s for FinSequence;

theorem Th28:
  t in F-entry_points_in_subformula_tree_of G & t^s in F
  -entry_points_in_subformula_tree_of H implies s in G
  -entry_points_in_subformula_tree_of H
proof
  defpred P[Element of NAT] means for F,G,H,t,s holds G = (tree_of_subformulae
  (F)).t & t^s in F-entry_points_in_subformula_tree_of H & len s = $1 implies s
  in G-entry_points_in_subformula_tree_of H;
A1: for k st P[k] holds P[k + 1]
  proof
    let k such that
A2: P[k];
    thus P[k + 1]
    proof
      let F,G,H,t,s;
      assume that
A3:   G = (tree_of_subformulae(F)).t and
A4:   t^s in F-entry_points_in_subformula_tree_of H and
A5:   len s = k+1;
      consider v being FinSequence, x being set such that
A6:   s = v^<*x*> and
A7:   len v = k by A5,TREES_2:3;
      F-entry_points_in_subformula_tree_of H = { t1 where t1 is Element
of dom tree_of_subformulae(F) : (tree_of_subformulae(F)).t1 = H } by Th19;
      then consider t99 such that
A8:   t99 = t^s and
A9:   (tree_of_subformulae(F)).t99 = H by A4;
      reconsider s1 = s as FinSequence of NAT by A8,FINSEQ_1:36;
A10:  s1 = v^<*x*> by A6;
      then reconsider u = <*x*> as FinSequence of NAT by FINSEQ_1:36;
      reconsider v as FinSequence of NAT by A10,FINSEQ_1:36;
A11:  rng u c= NAT by FINSEQ_1:def 4;
A12:  1 in {1} by TARSKI:def 1;
      dom u = Seg 1 & u.1 = x by FINSEQ_1:def 8;
      then x in rng u by A12,FINSEQ_1:2,FUNCT_1:def 3;
      then reconsider m = x as Element of NAT by A11;
      consider t9 being FinSequence of NAT such that
A13:  t9 = t^v;
A14:  t99 = t9^<*m*> by A6,A8,A13,FINSEQ_1:32;
      then t9 is_a_prefix_of t99 by TREES_1:1;
      then reconsider t9 as Element of dom tree_of_subformulae(F) by TREES_1:20
;
      consider H9 such that
A15:  H9 = (tree_of_subformulae(F)).t9;
      t^v in F-entry_points_in_subformula_tree_of H9 by A13,A15,Def3;
      then
A16:  v in G-entry_points_in_subformula_tree_of H9 by A2,A3,A7;
      G-entry_points_in_subformula_tree_of H9 = { v1 where v1 is Element
of dom tree_of_subformulae(G) : (tree_of_subformulae(G)).v1 = H9 } by Th19;
      then
A17:  ex v1 being Element of dom tree_of_subformulae(G) st v = v1 & (
      tree_of_subformulae(G)).v1 = H9 by A16;
      then reconsider v as Element of dom tree_of_subformulae(G);
A18:  H is_immediate_constituent_of H9 by A9,A14,A15,Th7;
      H = (tree_of_subformulae(G)).(v^<*m*>) & v^<*m*> in dom
      tree_of_subformulae(G)
      proof
A19:    H9 <> VERUM(A) by A18,QC_LANG2:41;
        now
          per cases by A18,A19,QC_LANG1:9,QC_LANG2:47;
          suppose
A20:        H9 is negative;
            then H = the_argument_of H9 & m = 0 by A9,A14,A15,Th21;
            hence thesis by A17,A20,Th24;
          end;
          suppose
A21:        H9 is conjunctive;
            then H = the_left_argument_of H9 & m = 0 or H =
            the_right_argument_of H9 & m = 1 by A9,A14,A15,Th22;
            hence thesis by A17,A21,Th25;
          end;
          suppose
A22:        H9 is universal;
            then H = the_scope_of H9 & m = 0 by A9,A14,A15,Th23;
            hence thesis by A17,A22,Th26;
          end;
        end;
        hence thesis;
      end;
      hence thesis by A6,Def3;
    end;
  end;
A23: P[0]
  proof
    let F,G,H,t,s;
    assume that
A24: G = (tree_of_subformulae(F)).t and
A25: t^s in F-entry_points_in_subformula_tree_of H and
A26: len s = 0;
A27: s = {} by A26;
    then reconsider s9 = s as Element of dom tree_of_subformulae(G) by
TREES_1:22;
A28: G = (tree_of_subformulae(G)).s9 by A27,Def2;
    F-entry_points_in_subformula_tree_of H = { t1 where t1 is Element of
    dom tree_of_subformulae(F) : (tree_of_subformulae(F)).t1 = H } by Th19;
    then ex t9 st t9 = t^s & (tree_of_subformulae(F)).t9 = H by A25;
    then H = G by A24,A27,FINSEQ_1:34;
    hence thesis by A28,Def3;
  end;
  for k holds P[k] from NAT_1:sch 1(A23,A1);
  then
A29: G = (tree_of_subformulae(F)).t & t^s in F
  -entry_points_in_subformula_tree_of H & len s = len s implies s in G
  -entry_points_in_subformula_tree_of H;
  assume t in F-entry_points_in_subformula_tree_of G & t^s in F
  -entry_points_in_subformula_tree_of H;
  hence thesis by A29,Def3;
end;

theorem Th29:
  for F,G,H holds { t^s where t is Element of dom
  tree_of_subformulae(F), s is Element of dom tree_of_subformulae(G) : t in F
  -entry_points_in_subformula_tree_of G & s in G
-entry_points_in_subformula_tree_of H } c= F-entry_points_in_subformula_tree_of
  H
proof
  let F,G,H;
  let x be set;
  assume x in { t^s where t is Element of dom tree_of_subformulae(F), s is
  Element of dom tree_of_subformulae(G) : t in F
  -entry_points_in_subformula_tree_of G & s in G
  -entry_points_in_subformula_tree_of H };
  then
  ex t being Element of dom tree_of_subformulae(F), s being Element of dom
tree_of_subformulae(G) st x = t^s & t in F -entry_points_in_subformula_tree_of
  G & s in G -entry_points_in_subformula_tree_of H;
  hence thesis by Th27;
end;

theorem Th30:
  (tree_of_subformulae(F))|t = tree_of_subformulae(( tree_of_subformulae(F)).t)
proof
  set T1 = (tree_of_subformulae(F))|t;
  set T2 = tree_of_subformulae((tree_of_subformulae(F)).t);
  thus
A1: dom T1 = dom T2
  proof
    let p be FinSequence of NAT;
    now
      consider G such that
A2:   G = (tree_of_subformulae(F)).t;
A3:   t in F-entry_points_in_subformula_tree_of G by A2,Def3;
      consider t9 being FinSequence of NAT such that
A4:   t9 = t^p;
      assume p in dom T1;
      then p in (dom tree_of_subformulae(F))|t by TREES_2:def 10;
      then reconsider t9 as Element of dom tree_of_subformulae(F) by A4,
TREES_1:def 6;
      consider H such that
A5:   H = (tree_of_subformulae(F)).t9;
A6:   G-entry_points_in_subformula_tree_of H c= dom T2 by A2,TREES_1:def 11;
      t9 in F-entry_points_in_subformula_tree_of H by A5,Def3;
      then p in G-entry_points_in_subformula_tree_of H by A3,A4,Th28;
      hence p in dom T2 by A6;
    end;
    hence p in dom T1 implies p in dom T2;
    now
      consider G such that
A7:   G = (tree_of_subformulae(F)).t;
      assume p in dom T2;
      then reconsider s = p as Element of dom tree_of_subformulae(G) by A7;
      consider H such that
A8:   H = (tree_of_subformulae(G)).s;
A9:   s in G-entry_points_in_subformula_tree_of H by A8,Def3;
A10:  F-entry_points_in_subformula_tree_of H c= dom tree_of_subformulae(F
      ) by TREES_1:def 11;
      t in F-entry_points_in_subformula_tree_of G by A7,Def3;
      then t^s in F-entry_points_in_subformula_tree_of H by A9,Th27;
      then s in (dom tree_of_subformulae(F))|t by A10,TREES_1:def 6;
      hence p in dom T1 by TREES_2:def 10;
    end;
    hence thesis;
  end;
  now
    let p be Node of T1;
    consider G such that
A11: G = (tree_of_subformulae(F)).t;
    reconsider s = p as Element of dom tree_of_subformulae(G) by A1,A11;
A12: dom T1 = (dom tree_of_subformulae(F))|t by TREES_2:def 10;
    then reconsider t9= t^s as Element of dom tree_of_subformulae(F) by
TREES_1:def 6;
    consider H such that
A13: H = T1.p;
A14: t in F-entry_points_in_subformula_tree_of G by A11,Def3;
    T1.p = (tree_of_subformulae(F)).(t^p) by A12,TREES_2:def 10;
    then t9 in F-entry_points_in_subformula_tree_of H by A13,Def3;
    then s in G-entry_points_in_subformula_tree_of H by A14,Th28;
    hence T1.p = T2.p by A11,A13,Def3;
  end;
  hence for p being Node of T1 holds T1.p = T2.p;
end;

theorem Th31:
  t in F-entry_points_in_subformula_tree_of G iff (
  tree_of_subformulae(F))|t = tree_of_subformulae(G)
proof
  now
    assume t in F-entry_points_in_subformula_tree_of G;
    then (tree_of_subformulae(F)).t = G by Def3;
    hence (tree_of_subformulae(F))|t = tree_of_subformulae(G) by Th30;
  end;
  hence t in F-entry_points_in_subformula_tree_of G implies (
  tree_of_subformulae(F))|t = tree_of_subformulae(G);
  now
    assume (tree_of_subformulae(F))|t = tree_of_subformulae(G);
    then
A1: (tree_of_subformulae(F)).t = (tree_of_subformulae(G)).{} by TREES_9:35;
    (tree_of_subformulae(G)).{} = G by Def2;
    hence t in F-entry_points_in_subformula_tree_of G by A1,Def3;
  end;
  hence thesis;
end;

theorem
  F-entry_points_in_subformula_tree_of G = { t where t is Element of dom
tree_of_subformulae(F) : (tree_of_subformulae(F))|t = tree_of_subformulae(G) }
proof
  thus F-entry_points_in_subformula_tree_of G c= { t where t is Element of dom
tree_of_subformulae(F) : (tree_of_subformulae(F))|t = tree_of_subformulae(G) }
  proof
    let x be set;
    assume
A1: x in F-entry_points_in_subformula_tree_of G;
    F-entry_points_in_subformula_tree_of G c= dom tree_of_subformulae(F)
    by TREES_1:def 11;
    then reconsider t9 = x as Element of dom tree_of_subformulae(F) by A1;
    (tree_of_subformulae(F))|t9 = tree_of_subformulae(G) by A1,Th31;
    hence thesis;
  end;
  thus { t where t is Element of dom tree_of_subformulae(F) : (
  tree_of_subformulae(F))|t = tree_of_subformulae(G) } c= F
  -entry_points_in_subformula_tree_of G
  proof
    let x be set;
    assume x in { t where t is Element of dom tree_of_subformulae(F) : (
    tree_of_subformulae(F))|t = tree_of_subformulae(G) };
    then
    ex t9 st t9 = x & (tree_of_subformulae(F))|t9 = tree_of_subformulae(G);
    hence thesis by Th31;
  end;
end;

reserve C for Chain of dom tree_of_subformulae(F);

theorem
  for F,G,H,C st G in { (tree_of_subformulae(F)).t where t is Element of
dom tree_of_subformulae(F) : t in C } & H in { (tree_of_subformulae(F)).t where
t is Element of dom tree_of_subformulae(F) : t in C } holds G is_subformula_of
  H or H is_subformula_of G
proof
  let F,G,H,C;
  assume that
A1: G in { (tree_of_subformulae(F)).t where t is Element of dom
  tree_of_subformulae(F) : t in C } and
A2: H in { (tree_of_subformulae(F)).t where t is Element of dom
  tree_of_subformulae(F) : t in C };
  consider t9 such that
A3: G = (tree_of_subformulae(F)).t9 and
A4: t9 in C by A1;
  consider t99 such that
A5: H = (tree_of_subformulae(F)).t99 and
A6: t99 in C by A2;
A7: t9,t99 are_c=-comparable by A4,A6,TREES_2:def 3;
  per cases by A7,XBOOLE_0:def 9;
  suppose
    t9 is_a_prefix_of t99;
    hence thesis by A3,A5,Th13;
  end;
  suppose
    t99 is_a_prefix_of t9;
    hence thesis by A3,A5,Th13;
  end;
end;

definition
  let A;
  let F be Element of QC-WFF(A);
  mode Subformula of F -> Element of QC-WFF(A) means
    :Def4:
    it is_subformula_of F;
  existence;
end;

definition
  let A;
  let F be Element of QC-WFF(A);
  let G be Subformula of F;
  mode Entry_Point_in_Subformula_Tree of G -> Element of dom
    tree_of_subformulae(F) means
    :Def5:
    (tree_of_subformulae(F)).it = G;
  existence
  proof
    G is_subformula_of F by Def4;
    then G in rng tree_of_subformulae(F) by Th10;
    then ex x being set st x in dom tree_of_subformulae(F) & (
    tree_of_subformulae(F)).x = G by FUNCT_1:def 3;
    hence thesis;
  end;
end;

reserve G for Subformula of F;
reserve t, t9 for Entry_Point_in_Subformula_Tree of G;

theorem
  t <> t9 implies not t,t9 are_c=-comparable
proof
  assume
A1: t <> t9;
  (tree_of_subformulae(F)).t = G & (tree_of_subformulae(F)).t9 = G by Def5;
  hence thesis by A1,Th18;
end;

definition
  let A;
  let F be Element of QC-WFF(A);
  let G be Subformula of F;
  func entry_points_in_subformula_tree(G) -> non empty AntiChain_of_Prefixes
  of dom tree_of_subformulae(F) equals
  F-entry_points_in_subformula_tree_of G;
  coherence
  proof
    G is_subformula_of F by Def4;
    hence thesis by Th20;
  end;
end;

theorem Th35:
  t in entry_points_in_subformula_tree(G)
proof
  (tree_of_subformulae(F)).t = G by Def5;
  hence thesis by Def3;
end;

theorem Th36:
  entry_points_in_subformula_tree(G) = { t where t is
  Entry_Point_in_Subformula_Tree of G : t = t }
proof
  thus entry_points_in_subformula_tree(G) c= { t where t is
  Entry_Point_in_Subformula_Tree of G : t = t }
  proof
    let x be set;
    assume x in entry_points_in_subformula_tree(G);
    then x in { t where t is Element of dom tree_of_subformulae(F) : (
    tree_of_subformulae(F)).t = G } by Th19;
    then consider t9 being Element of dom tree_of_subformulae(F) such that
A1: t9 = x and
A2: (tree_of_subformulae(F)).t9 = G;
    reconsider t9 as Entry_Point_in_Subformula_Tree of G by A2,Def5;
    t9 = t9;
    hence thesis by A1;
  end;
  thus { t where t is Entry_Point_in_Subformula_Tree of G : t = t } c=
  entry_points_in_subformula_tree(G)
  proof
    let x be set;
    assume x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t };
    then ex t st t = x & t = t;
    hence thesis by Th35;
  end;
end;

reserve G1, G2 for Subformula of F,
  t1 for Entry_Point_in_Subformula_Tree of G1,
  s for Element of dom tree_of_subformulae(G1);

theorem Th37:
  s in G1-entry_points_in_subformula_tree_of G2 implies t1^s is
  Entry_Point_in_Subformula_Tree of G2
proof
  (tree_of_subformulae(F)).t1 = G1 by Def5;
  then
A1: t1 in F-entry_points_in_subformula_tree_of G1 by Def3;
  assume s in G1-entry_points_in_subformula_tree_of G2;
  then
A2: t1^s in F-entry_points_in_subformula_tree_of G2 by A1,Th27;
  F-entry_points_in_subformula_tree_of G2 c= dom tree_of_subformulae(F) by
TREES_1:def 11;
  then reconsider t9 = t1^s as Element of dom tree_of_subformulae(F) by A2;
  (tree_of_subformulae(F)).t9 = G2 by A2,Def3;
  hence thesis by Def5;
end;

reserve s for FinSequence;

theorem
  t1^s is Entry_Point_in_Subformula_Tree of G2 implies s in G1
  -entry_points_in_subformula_tree_of G2
proof
  consider t9 being FinSequence such that
A1: t9 = t1^s;
  (tree_of_subformulae(F)).t1 = G1 by Def5;
  then
A2: t1 in F-entry_points_in_subformula_tree_of G1 by Def3;
  assume t1^s is Entry_Point_in_Subformula_Tree of G2;
  then
  t9 in { t2 where t2 is Entry_Point_in_Subformula_Tree of G2 : t2 = t2 }
  by A1;
  then t9 in entry_points_in_subformula_tree(G2) by Th36;
  hence thesis by A2,A1,Th28;
end;

theorem Th39:
  for F,G1,G2 holds { t^s where t is
Entry_Point_in_Subformula_Tree of G1, s is Element of dom tree_of_subformulae(
  G1) : s in G1-entry_points_in_subformula_tree_of G2 } = { t^s where t is
Element of dom tree_of_subformulae(F), s is Element of dom tree_of_subformulae(
  G1) : t in F-entry_points_in_subformula_tree_of G1 & s in G1
  -entry_points_in_subformula_tree_of G2 }
proof
  let F,G1,G2;
  thus { t^s where t is Entry_Point_in_Subformula_Tree of G1, s is Element of
  dom tree_of_subformulae(G1) : s in G1-entry_points_in_subformula_tree_of G2 }
c= { t^s where t is Element of dom tree_of_subformulae(F), s is Element of dom
  tree_of_subformulae(G1) : t in F-entry_points_in_subformula_tree_of G1 & s in
  G1-entry_points_in_subformula_tree_of G2 }
  proof
    let x be set;
    assume x in { t^s where t is Entry_Point_in_Subformula_Tree of G1, s is
    Element of dom tree_of_subformulae(G1) : s in G1
    -entry_points_in_subformula_tree_of G2 };
    then consider
    t1 being Entry_Point_in_Subformula_Tree of G1, s1 being Element
    of dom tree_of_subformulae(G1) such that
A1: x = t1^s1 & s1 in G1-entry_points_in_subformula_tree_of G2;
    (tree_of_subformulae(F)).t1 = G1 by Def5;
    then t1 in F-entry_points_in_subformula_tree_of G1 by Def3;
    hence thesis by A1;
  end;
  thus { t^s where t is Element of dom tree_of_subformulae(F), s is Element of
dom tree_of_subformulae(G1) : t in F-entry_points_in_subformula_tree_of G1 & s
  in G1-entry_points_in_subformula_tree_of G2 } c= { t^s where t is
Entry_Point_in_Subformula_Tree of G1, s is Element of dom tree_of_subformulae(
  G1) : s in G1-entry_points_in_subformula_tree_of G2 }
  proof
    let x be set;
    assume x in { t^s where t is Element of dom tree_of_subformulae(F), s is
    Element of dom tree_of_subformulae(G1) : t in F
    -entry_points_in_subformula_tree_of G1 & s in G1
    -entry_points_in_subformula_tree_of G2 };
    then consider
    t1 being Element of dom tree_of_subformulae(F), s1 being Element
    of dom tree_of_subformulae(G1) such that
A2: x = t1^s1 and
A3: t1 in F-entry_points_in_subformula_tree_of G1 and
A4: s1 in G1-entry_points_in_subformula_tree_of G2;
    (tree_of_subformulae(F)).t1 = G1 by A3,Def3;
    then reconsider t1 as Entry_Point_in_Subformula_Tree of G1 by Def5;
    x = t1^s1 by A2;
    hence thesis by A4;
  end;
end;

theorem
  for F,G1,G2 holds { t^s where t is Entry_Point_in_Subformula_Tree of
  G1, s is Element of dom tree_of_subformulae(G1) : s in G1
-entry_points_in_subformula_tree_of G2 } c= entry_points_in_subformula_tree(G2)
proof
  let F,G1,G2;
  { t^s where t is Entry_Point_in_Subformula_Tree of G1, s is Element of
dom tree_of_subformulae(G1) : s in G1-entry_points_in_subformula_tree_of G2 } =
  { t^s where t is Element of dom tree_of_subformulae(F), s is Element of dom
  tree_of_subformulae(G1) : t in F-entry_points_in_subformula_tree_of G1 & s in
  G1-entry_points_in_subformula_tree_of G2 } by Th39;
  hence thesis by Th29;
end;

reserve G1, G2 for Subformula of F,
  t1 for Entry_Point_in_Subformula_Tree of G1,
  t2 for Entry_Point_in_Subformula_Tree of G2;

theorem
  (ex t1,t2 st t1 is_a_prefix_of t2) implies G2 is_subformula_of G1
proof
  given t1,t2 such that
A1: t1 is_a_prefix_of t2;
  (tree_of_subformulae(F)).t1 = G1 & (tree_of_subformulae(F)).t2 = G2 by Def5;
  hence thesis by A1,Th13;
end;

theorem
  G2 is_subformula_of G1 implies for t1 ex t2 st t1 is_a_prefix_of t2
proof
  assume
A1: G2 is_subformula_of G1;
  now
    let t1;
    consider H being Element of QC-WFF(A) such that
A2: H = G2;
    reconsider H as Subformula of G1 by A1,A2,Def4;
    set s = the Entry_Point_in_Subformula_Tree of H;
    (tree_of_subformulae(G1)).s = H by Def5;
    then s in G1-entry_points_in_subformula_tree_of G2 by A2,Def3;
    then t1^s is Entry_Point_in_Subformula_Tree of G2 by Th37;
    then consider t2 such that
A3: t2 = t1^s;
    take t2;
    thus t1 is_a_prefix_of t2 by A3,TREES_1:1;
  end;
  hence thesis;
end;