qc_lang2.miz



    begin

    reserve A for QC-alphabet;

    reserve sq for FinSequence,

x,y,z for bound_QC-variable of A,

p,q,p1,p2,q1 for Element of ( QC-WFF A);

    theorem :: QC_LANG2:1

    

     Th1: ( the_argument_of ( 'not' p)) = p

    proof

      ( 'not' p) is negative;

      hence thesis by QC_LANG1:def 24;

    end;

    theorem :: QC_LANG2:2

    

     Th2: (p '&' q) = (p1 '&' q1) implies p = p1 & q = q1

    proof

      assume

       A1: (p '&' q) = (p1 '&' q1);

      (( <* [2, 0 ]*> ^ ( @ p)) ^ ( @ q)) = ( <* [2, 0 ]*> ^ (( @ p) ^ ( @ q))) & (( <* [2, 0 ]*> ^ ( @ p1)) ^ ( @ q1)) = ( <* [2, 0 ]*> ^ (( @ p1) ^ ( @ q1))) by FINSEQ_1: 32;

      then

       A2: (( @ p) ^ ( @ q)) = (( @ p1) ^ ( @ q1)) by A1, FINSEQ_1: 33;

      then

       A3: ( len ( @ p1)) <= ( len ( @ p)) implies ex sq st ( @ p) = (( @ p1) ^ sq) by FINSEQ_1: 47;

      

       A4: ( len ( @ p)) <= ( len ( @ p1)) implies ex sq st ( @ p1) = (( @ p) ^ sq) by A2, FINSEQ_1: 47;

      hence p = p1 by A3, QC_LANG1: 13;

      (ex sq st ( @ p1) = (( @ p) ^ sq)) implies p1 = p by QC_LANG1: 13;

      hence thesis by A1, A3, A4, FINSEQ_1: 33, QC_LANG1: 13;

    end;

    theorem :: QC_LANG2:3

    

     Th3: p is conjunctive implies p = (( the_left_argument_of p) '&' ( the_right_argument_of p))

    proof

      given p1, q1 such that

       A1: p = (p1 '&' q1);

      

       A2: p is conjunctive by A1;

      then p1 = ( the_left_argument_of p) by A1, QC_LANG1:def 25;

      hence thesis by A1, A2, QC_LANG1:def 26;

    end;

    theorem :: QC_LANG2:4

    

     Th4: ( the_left_argument_of (p '&' q)) = p & ( the_right_argument_of (p '&' q)) = q

    proof

      (p '&' q) is conjunctive;

      hence thesis by QC_LANG1:def 25, QC_LANG1:def 26;

    end;

    theorem :: QC_LANG2:5

    

     Th5: ( All (x,p)) = ( All (y,q)) implies x = y & p = q

    proof

      

       A1: (( <* [3, 0 ]*> ^ <*x*>) ^ ( @ p)) = ( <* [3, 0 ]*> ^ ( <*x*> ^ ( @ p))) & (( <* [3, 0 ]*> ^ <*y*>) ^ ( @ q)) = ( <* [3, 0 ]*> ^ ( <*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;

    theorem :: QC_LANG2:6

    

     Th6: p is universal implies p = ( All (( bound_in p),( the_scope_of p)))

    proof

      given x, q such that

       A1: p = ( All (x,q));

      

       A2: p is universal by A1;

      then x = ( bound_in p) by A1, QC_LANG1:def 27;

      hence thesis by A1, A2, QC_LANG1:def 28;

    end;

    theorem :: QC_LANG2:7

    

     Th7: ( bound_in ( All (x,p))) = x & ( the_scope_of ( All (x,p))) = p

    proof

      ( All (x,p)) is universal;

      then ( All (x,p)) = ( All (( bound_in ( All (x,p))),( the_scope_of ( All (x,p))))) by Th6;

      hence thesis by Th5;

    end;

    definition

      let A be QC-alphabet;

      :: QC_LANG2:def1

      func FALSUM (A) -> QC-formula of A equals ( 'not' ( VERUM A));

      correctness ;

      let p,q be Element of ( QC-WFF A);

      :: QC_LANG2:def2

      func p => q -> QC-formula of A equals ( 'not' (p '&' ( 'not' q)));

      correctness ;

      :: QC_LANG2:def3

      func p 'or' q -> QC-formula of A equals ( 'not' (( 'not' p) '&' ( 'not' q)));

      correctness ;

    end

    definition

      let A be QC-alphabet;

      let p,q be Element of ( QC-WFF A);

      :: QC_LANG2:def4

      func p <=> q -> QC-formula of A equals ((p => q) '&' (q => p));

      correctness ;

    end

    definition

      let A be QC-alphabet;

      let x be bound_QC-variable of A, p be Element of ( QC-WFF A);

      :: QC_LANG2:def5

      func Ex (x,p) -> QC-formula of A equals ( 'not' ( All (x,( 'not' p))));

      correctness ;

    end

    theorem :: QC_LANG2:8

    ( FALSUM A) is negative & ( the_argument_of ( FALSUM A)) = ( VERUM A) by Th1;

    theorem :: QC_LANG2:9

    (p 'or' q) = (( 'not' p) => q);

    theorem :: QC_LANG2:10

    (p 'or' q) = (p1 'or' q1) implies p = p1 & q = q1

    proof

      assume (p 'or' q) = (p1 'or' q1);

      then (( 'not' p) '&' ( 'not' q)) = (( 'not' p1) '&' ( 'not' q1)) by FINSEQ_1: 33;

      then ( 'not' p) = ( 'not' p1) & ( 'not' q) = ( 'not' q1) by Th2;

      hence thesis by FINSEQ_1: 33;

    end;

    theorem :: QC_LANG2:11

    

     Th11: (p => q) = (p1 => q1) implies p = p1 & q = q1

    proof

      assume (p => q) = (p1 => q1);

      then

       A1: (p '&' ( 'not' q)) = (p1 '&' ( 'not' q1)) by FINSEQ_1: 33;

      hence p = p1 by Th2;

      ( 'not' q) = ( 'not' q1) by A1, Th2;

      hence thesis by FINSEQ_1: 33;

    end;

    theorem :: QC_LANG2:12

    (p <=> q) = (p1 <=> q1) implies p = p1 & q = q1

    proof

      assume (p <=> q) = (p1 <=> q1);

      then (p => q) = (p1 => q1) by Th2;

      hence thesis by Th11;

    end;

    theorem :: QC_LANG2:13

    

     Th13: ( Ex (x,p)) = ( Ex (y,q)) implies x = y & p = q

    proof

      assume ( Ex (x,p)) = ( Ex (y,q));

      then

       A1: ( All (x,( 'not' p))) = ( All (y,( 'not' q))) by FINSEQ_1: 33;

      then ( 'not' p) = ( 'not' q) by Th5;

      hence thesis by A1, Th5, FINSEQ_1: 33;

    end;

    definition

      let A be QC-alphabet;

      let x,y be bound_QC-variable of A, p be Element of ( QC-WFF A);

      :: QC_LANG2:def6

      func All (x,y,p) -> QC-formula of A equals ( All (x,( All (y,p))));

      correctness ;

      :: QC_LANG2:def7

      func Ex (x,y,p) -> QC-formula of A equals ( Ex (x,( Ex (y,p))));

      correctness ;

    end

    theorem :: QC_LANG2:14

    ( All (x,y,p)) = ( All (x,( All (y,p)))) & ( Ex (x,y,p)) = ( Ex (x,( Ex (y,p))));

    theorem :: QC_LANG2:15

    

     Th15: for x1,x2,y1,y2 be bound_QC-variable of A st ( All (x1,y1,p1)) = ( All (x2,y2,p2)) holds x1 = x2 & y1 = y2 & p1 = p2

    proof

      let x1,x2,y1,y2 be bound_QC-variable of A such that

       A1: ( All (x1,y1,p1)) = ( All (x2,y2,p2));

      thus x1 = x2 by A1, Th5;

      ( All (y1,p1)) = ( All (y2,p2)) by A1, Th5;

      hence thesis by Th5;

    end;

    theorem :: QC_LANG2:16

    ( All (x,y,p)) = ( All (z,q)) implies x = z & ( All (y,p)) = q by Th5;

    theorem :: QC_LANG2:17

    

     Th17: for x1,x2,y1,y2 be bound_QC-variable of A st ( Ex (x1,y1,p1)) = ( Ex (x2,y2,p2)) holds x1 = x2 & y1 = y2 & p1 = p2

    proof

      let x1,x2,y1,y2 be bound_QC-variable of A such that

       A1: ( Ex (x1,y1,p1)) = ( Ex (x2,y2,p2));

      thus x1 = x2 by A1, Th13;

      ( Ex (y1,p1)) = ( Ex (y2,p2)) by A1, Th13;

      hence thesis by Th13;

    end;

    theorem :: QC_LANG2:18

    ( Ex (x,y,p)) = ( Ex (z,q)) implies x = z & ( Ex (y,p)) = q by Th13;

    theorem :: QC_LANG2:19

    ( All (x,y,p)) is universal & ( bound_in ( All (x,y,p))) = x & ( the_scope_of ( All (x,y,p))) = ( All (y,p)) by Th7;

    definition

      let A be QC-alphabet;

      let x,y,z be bound_QC-variable of A, p be Element of ( QC-WFF A);

      :: QC_LANG2:def8

      func All (x,y,z,p) -> QC-formula of A equals ( All (x,( All (y,z,p))));

      correctness ;

      :: QC_LANG2:def9

      func Ex (x,y,z,p) -> QC-formula of A equals ( Ex (x,( Ex (y,z,p))));

      correctness ;

    end

    theorem :: QC_LANG2:20

    ( All (x,y,z,p)) = ( All (x,( All (y,z,p)))) & ( Ex (x,y,z,p)) = ( Ex (x,( Ex (y,z,p))));

    theorem :: QC_LANG2:21

    for x1,x2,y1,y2,z1,z2 be bound_QC-variable of A st ( All (x1,y1,z1,p1)) = ( All (x2,y2,z2,p2)) holds x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2

    proof

      let x1,x2,y1,y2,z1,z2 be bound_QC-variable of A such that

       A1: ( All (x1,y1,z1,p1)) = ( All (x2,y2,z2,p2));

      thus x1 = x2 by A1, Th5;

      ( All (y1,z1,p1)) = ( All (y2,z2,p2)) by A1, Th5;

      hence thesis by Th15;

    end;

    reserve s,t for bound_QC-variable of A;

    theorem :: QC_LANG2:22

    ( All (x,y,z,p)) = ( All (t,q)) implies x = t & ( All (y,z,p)) = q by Th5;

    theorem :: QC_LANG2:23

    ( All (x,y,z,p)) = ( All (t,s,q)) implies x = t & y = s & ( All (z,p)) = q

    proof

      assume

       A1: ( All (x,y,z,p)) = ( All (t,s,q));

      hence x = t by Th5;

      ( All (y,z,p)) = ( All (s,q)) by A1, Th5;

      hence thesis by Th5;

    end;

    theorem :: QC_LANG2:24

    for x1,x2,y1,y2,z1,z2 be bound_QC-variable of A st ( Ex (x1,y1,z1,p1)) = ( Ex (x2,y2,z2,p2)) holds x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2

    proof

      let x1,x2,y1,y2,z1,z2 be bound_QC-variable of A such that

       A1: ( Ex (x1,y1,z1,p1)) = ( Ex (x2,y2,z2,p2));

      thus x1 = x2 by A1, Th13;

      ( Ex (y1,z1,p1)) = ( Ex (y2,z2,p2)) by A1, Th13;

      hence thesis by Th17;

    end;

    theorem :: QC_LANG2:25

    ( Ex (x,y,z,p)) = ( Ex (t,q)) implies x = t & ( Ex (y,z,p)) = q by Th13;

    theorem :: QC_LANG2:26

    ( Ex (x,y,z,p)) = ( Ex (t,s,q)) implies x = t & y = s & ( Ex (z,p)) = q

    proof

      assume

       A1: ( Ex (x,y,z,p)) = ( Ex (t,s,q));

      hence x = t by Th13;

      ( Ex (y,z,p)) = ( Ex (s,q)) by A1, Th13;

      hence thesis by Th13;

    end;

    theorem :: QC_LANG2:27

    ( All (x,y,z,p)) is universal & ( bound_in ( All (x,y,z,p))) = x & ( the_scope_of ( All (x,y,z,p))) = ( All (y,z,p)) by Th7;

    definition

      let A be QC-alphabet;

      let H be Element of ( QC-WFF A);

      :: QC_LANG2:def10

      attr H is disjunctive means ex p,q be Element of ( QC-WFF A) st H = (p 'or' q);

      :: QC_LANG2:def11

      attr H is conditional means ex p,q be Element of ( QC-WFF A) st H = (p => q);

      :: QC_LANG2:def12

      attr H is biconditional means ex p,q be Element of ( QC-WFF A) st H = (p <=> q);

      :: QC_LANG2:def13

      attr H is existential means ex x be bound_QC-variable of A, p be Element of ( QC-WFF A) st H = ( Ex (x,p));

    end

    theorem :: QC_LANG2:28

    ( Ex (x,y,p)) is existential & ( Ex (x,y,z,p)) is existential;

    definition

      let A be QC-alphabet;

      let H be Element of ( QC-WFF A);

      :: QC_LANG2:def14

      func the_left_disjunct_of H -> QC-formula of A equals ( the_argument_of ( the_left_argument_of ( the_argument_of H)));

      correctness ;

      :: QC_LANG2:def15

      func the_right_disjunct_of H -> QC-formula of A equals ( the_argument_of ( the_right_argument_of ( the_argument_of H)));

      correctness ;

      :: QC_LANG2:def16

      func the_antecedent_of H -> QC-formula of A equals ( the_left_argument_of ( the_argument_of H));

      correctness ;

    end

    notation

      let A be QC-alphabet;

      let H be Element of ( QC-WFF A);

      synonym the_consequent_of H for the_right_disjunct_of H;

    end

    definition

      let A be QC-alphabet;

      let H be Element of ( QC-WFF A);

      :: QC_LANG2:def17

      func the_left_side_of H -> QC-formula of A equals ( the_antecedent_of ( the_left_argument_of H));

      correctness ;

      :: QC_LANG2:def18

      func the_right_side_of H -> QC-formula of A equals ( the_consequent_of ( the_left_argument_of H));

      correctness ;

    end

    reserve F,G,H,H1 for Element of ( QC-WFF A);

    theorem :: QC_LANG2:29

    

     Th29: ( the_left_disjunct_of (F 'or' G)) = F & ( the_right_disjunct_of (F 'or' G)) = G & ( the_argument_of (F 'or' G)) = (( 'not' F) '&' ( 'not' G))

    proof

      

      thus ( the_left_disjunct_of (F 'or' G)) = ( the_argument_of ( the_left_argument_of (( 'not' F) '&' ( 'not' G)))) by Th1

      .= ( the_argument_of ( 'not' F)) by Th4

      .= F by Th1;

      

      thus ( the_right_disjunct_of (F 'or' G)) = ( the_argument_of ( the_right_argument_of (( 'not' F) '&' ( 'not' G)))) by Th1

      .= ( the_argument_of ( 'not' G)) by Th4

      .= G by Th1;

      thus thesis by Th1;

    end;

    theorem :: QC_LANG2:30

    

     Th30: ( the_antecedent_of (F => G)) = F & ( the_consequent_of (F => G)) = G & ( the_argument_of (F => G)) = (F '&' ( 'not' G))

    proof

      

      thus ( the_antecedent_of (F => G)) = ( the_left_argument_of (F '&' ( 'not' G))) by Th1

      .= F by Th4;

      

      thus ( the_consequent_of (F => G)) = ( the_argument_of ( the_right_argument_of (F '&' ( 'not' G)))) by Th1

      .= ( the_argument_of ( 'not' G)) by Th4

      .= G by Th1;

      thus thesis by Th1;

    end;

    theorem :: QC_LANG2:31

    

     Th31: ( the_left_side_of (F <=> G)) = F & ( the_right_side_of (F <=> G)) = G & ( the_left_argument_of (F <=> G)) = (F => G) & ( the_right_argument_of (F <=> G)) = (G => F)

    proof

      ( the_antecedent_of (F => G)) = F & ( the_consequent_of (F => G)) = G by Th30;

      hence thesis by Th4;

    end;

    theorem :: QC_LANG2:32

    ( the_argument_of ( Ex (x,H))) = ( All (x,( 'not' H))) by Th1;

    theorem :: QC_LANG2:33

    H is disjunctive implies H is conditional & H is negative & ( the_argument_of H) is conjunctive & ( the_left_argument_of ( the_argument_of H)) is negative & ( the_right_argument_of ( the_argument_of H)) is negative

    proof

      given F, G such that

       A1: H = (F 'or' G);

      (F 'or' G) = (( 'not' F) => G);

      hence H is conditional by A1;

      thus H is negative by A1;

      

       A2: ( the_argument_of H) = (( 'not' F) '&' ( 'not' G)) by A1, Th1;

      hence ( the_argument_of H) is conjunctive;

      ( the_left_argument_of ( the_argument_of H)) = ( 'not' F) & ( the_right_argument_of ( the_argument_of H)) = ( 'not' G) by A2, Th4;

      hence thesis;

    end;

    theorem :: QC_LANG2:34

    H is conditional implies H is negative & ( the_argument_of H) is conjunctive & ( the_right_argument_of ( the_argument_of H)) is negative

    proof

      given F, G such that

       A1: H = (F => G);

      ( the_argument_of ( 'not' (F '&' ( 'not' G)))) = (F '&' ( 'not' G)) & ( the_right_argument_of (F '&' ( 'not' G))) = ( 'not' G) by Th1, Th4;

      hence thesis by A1;

    end;

    theorem :: QC_LANG2:35

    H is biconditional implies H is conjunctive & ( the_left_argument_of H) is conditional & ( the_right_argument_of H) is conditional by Th4;

    theorem :: QC_LANG2:36

    H is existential implies H is negative & ( the_argument_of H) is universal & ( the_scope_of ( the_argument_of H)) is negative

    proof

      given x, H1 such that

       A1: H = ( Ex (x,H1));

      ( the_argument_of ( 'not' ( All (x,( 'not' H1))))) = ( All (x,( 'not' H1))) & ( the_scope_of ( All (x,( 'not' H1)))) = ( 'not' H1) by Th1, Th7;

      hence thesis by A1;

    end;

    theorem :: QC_LANG2:37

    H is disjunctive implies H = (( the_left_disjunct_of H) 'or' ( the_right_disjunct_of H))

    proof

      given F, G such that

       A1: H = (F 'or' G);

      ( the_left_disjunct_of H) = F by A1, Th29;

      hence thesis by A1, Th29;

    end;

    theorem :: QC_LANG2:38

    H is conditional implies H = (( the_antecedent_of H) => ( the_consequent_of H))

    proof

      given F, G such that

       A1: H = (F => G);

      ( the_antecedent_of H) = F by A1, Th30;

      hence thesis by A1, Th30;

    end;

    theorem :: QC_LANG2:39

    H is biconditional implies H = (( the_left_side_of H) <=> ( the_right_side_of H))

    proof

      given F, G such that

       A1: H = (F <=> G);

      ( the_left_side_of H) = F by A1, Th31;

      hence thesis by A1, Th31;

    end;

    theorem :: QC_LANG2:40

    H is existential implies H = ( Ex (( bound_in ( the_argument_of H)),( the_argument_of ( the_scope_of ( the_argument_of H)))))

    proof

      given x, H1 such that

       A1: H = ( Ex (x,H1));

      

       A2: ( the_argument_of ( 'not' H1)) = H1 by Th1;

      ( the_argument_of ( 'not' ( All (x,( 'not' H1))))) = ( All (x,( 'not' H1))) & ( the_scope_of ( All (x,( 'not' H1)))) = ( 'not' H1) by Th1, Th7;

      hence thesis by A1, A2, Th7;

    end;

    definition

      let A be QC-alphabet;

      let G,H be Element of ( QC-WFF A);

      :: QC_LANG2:def19

      pred G is_immediate_constituent_of H means H = ( 'not' G) or (ex F be Element of ( QC-WFF A) st H = (G '&' F) or H = (F '&' G)) or ex x be bound_QC-variable of A st H = ( All (x,G));

    end

    reserve x,y,z for bound_QC-variable of A,

k,n,m for Nat,

P for QC-pred_symbol of k, A,

V for QC-variable_list of k, A;

    theorem :: QC_LANG2:41

    

     Th41: not H is_immediate_constituent_of ( VERUM A)

    proof

       not (( VERUM A) is negative or ( VERUM A) is conjunctive or ( VERUM A) is universal) by QC_LANG1: 20;

      then not ((( VERUM A) = ( 'not' H)) or (ex H1 st ( VERUM A) = (H '&' H1) or ( VERUM A) = (H1 '&' H)) or (ex x be bound_QC-variable of A st ( VERUM A) = ( All (x,H))));

      hence thesis;

    end;

    theorem :: QC_LANG2:42

    

     Th42: not H is_immediate_constituent_of (P ! V)

    proof

      assume

       A1: not thesis;

      

       A2: (P ! V) is atomic;

      then

       A3: ((( @ (P ! V)) . 1) `1 ) <> 3 by QC_LANG1: 19;

      

       A4: ((( @ (P ! V)) . 1) `1 ) <> 2 by A2, QC_LANG1: 19;

      

       A5: not ex H1 be Element of ( QC-WFF A) st (P ! V) = (H '&' H1) or (P ! V) = (H1 '&' H) by A4, QC_LANG1: 18, QC_LANG1:def 20;

      ( 'not' H) is negative;

      then

       A6: ((( @ ( 'not' H)) . 1) `1 ) = 1 by QC_LANG1: 18;

      ((( @ (P ! V)) . 1) `1 ) <> 1 by A2, QC_LANG1: 19;

      then

      consider z such that

       A7: (P ! V) = ( All (z,H)) by A1, A6, A5;

      ( All (z,H)) is universal;

      hence contradiction by A3, A7, QC_LANG1: 18;

    end;

    theorem :: QC_LANG2:43

    

     Th43: F is_immediate_constituent_of ( 'not' H) iff F = H

    proof

      thus F is_immediate_constituent_of ( 'not' H) implies F = H

      proof

        ( 'not' H) is negative;

        then

         A1: ((( @ ( 'not' H)) . 1) `1 ) = 1 by QC_LANG1: 18;

        

         A2: not ex H1 st ( 'not' H) = (F '&' H1) or ( 'not' H) = (H1 '&' F) by A1, QC_LANG1: 18, QC_LANG1:def 20;

        

         A3: not ex x st ( 'not' H) = ( All (x,F)) by A1, QC_LANG1: 18, QC_LANG1:def 21;

        assume ( '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));

        hence thesis by A2, A3, FINSEQ_1: 33;

      end;

      thus thesis;

    end;

    theorem :: QC_LANG2:44

    H is_immediate_constituent_of ( FALSUM A) iff H = ( VERUM A) by Th43;

    theorem :: QC_LANG2:45

    

     Th45: 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

        (G '&' H) is conjunctive;

        then

         A1: ((( @ (G '&' H)) . 1) `1 ) = 2 by QC_LANG1: 18;

        

         A2: (G '&' H) <> ( 'not' F) by A1, QC_LANG1: 18, QC_LANG1:def 19;

        

         A3: not ex x st (G '&' H) = ( All (x,F)) by A1, QC_LANG1: 18, QC_LANG1:def 21;

        assume (G '&' H) = ( 'not' F) or (ex H1 st (G '&' H) = (F '&' H1) or (G '&' H) = (H1 '&' F)) or ex x st (G '&' H) = ( All (x,F));

        hence thesis by A2, A3, Th2;

      end;

      assume F = G or F = H;

      hence thesis;

    end;

    theorem :: QC_LANG2:46

    

     Th46: 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

        ( All (x,H)) is universal;

        then

         A1: ((( @ ( All (x,H))) . 1) `1 ) = 3 by QC_LANG1: 18;

        

         A2: ( All (x,H)) <> ( 'not' F) by A1, QC_LANG1: 18, QC_LANG1:def 19;

        

         A3: not ex G st ( All (x,H)) = (F '&' G) or ( All (x,H)) = (G '&' F) by A1, QC_LANG1: 18, QC_LANG1:def 20;

        assume ( All (x,H)) = ( 'not' F) or (ex H1 st ( All (x,H)) = (F '&' H1) or ( All (x,H)) = (H1 '&' F)) or ex y st ( All (x,H)) = ( All (y,F));

        hence thesis by A2, A3, Th5;

      end;

      thus thesis;

    end;

    theorem :: QC_LANG2:47

    

     Th47: H is atomic implies not F is_immediate_constituent_of H by Th42;

    theorem :: QC_LANG2:48

    

     Th48: 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 QC_LANG1:def 24;

      hence thesis by Th43;

    end;

    theorem :: QC_LANG2:49

    

     Th49: 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 Th3;

      hence thesis by Th45;

    end;

    theorem :: QC_LANG2:50

    

     Th50: 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 Th6;

      hence thesis by Th46;

    end;

    reserve L,L9 for FinSequence;

    definition

      let A be QC-alphabet;

      let G,H be Element of ( QC-WFF A);

      :: QC_LANG2:def20

      pred G is_subformula_of H means ex n, L st 1 <= n & ( len L) = n & (L . 1) = G & (L . n) = H & for k st 1 <= k & k < n holds ex G1,H1 be Element of ( QC-WFF A) st (L . k) = G1 & (L . (k + 1)) = H1 & G1 is_immediate_constituent_of H1;

      reflexivity

      proof

        let H be Element of ( QC-WFF A);

        reconsider L = <*H*> as FinSequence;

        take 1, L;

        thus 1 <= 1 & ( len L) = 1 & (L . 1) = H & (L . 1) = H by FINSEQ_1: 40;

        let k;

        assume 1 <= k & k < 1;

        hence thesis;

      end;

    end

    definition

      let A be QC-alphabet;

      let H,F be Element of ( QC-WFF A);

      :: QC_LANG2:def21

      pred H is_proper_subformula_of F means

      : Def21: H is_subformula_of F & H <> F;

      irreflexivity ;

    end

    theorem :: QC_LANG2:51

    

     Th51: H is_immediate_constituent_of F implies ( len ( @ H)) < ( len ( @ F))

    proof

      

       A1: F = ( VERUM A) or F is atomic or F is negative or F is conjunctive or F is universal by QC_LANG1: 9;

      assume H is_immediate_constituent_of F;

      then F is negative & H = ( the_argument_of F) or F is conjunctive & H = ( the_left_argument_of F) or F is conjunctive & H = ( the_right_argument_of F) or F is universal & H = ( the_scope_of F) by A1, Th41, Th47, Th48, Th49, Th50;

      hence thesis by QC_LANG1: 14, QC_LANG1: 15, QC_LANG1: 16;

    end;

    theorem :: QC_LANG2:52

    

     Th52: H is_immediate_constituent_of F implies H is_subformula_of F

    proof

      assume

       A1: H is_immediate_constituent_of F;

      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;

    theorem :: QC_LANG2:53

    

     Th53: H is_immediate_constituent_of F implies H is_proper_subformula_of F

    proof

      assume

       A1: H is_immediate_constituent_of F;

      hence H is_subformula_of F by Th52;

      assume H = F;

      then ( len ( @ H)) = ( len ( @ F));

      hence contradiction by A1, Th51;

    end;

    theorem :: QC_LANG2:54

    

     Th54: H is_proper_subformula_of F implies ( len ( @ H)) < ( len ( @ F))

    proof

      given 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 holds ex H1,F1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = F1 & H1 is_immediate_constituent_of F1;

      defpred P[ 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 be Element of ( QC-WFF A) 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, NAT_1: 13;

          hence thesis by A11, A10, Th51, XXREAL_0: 2;

        end;

        k = 0 implies ( len ( @ H)) < ( len ( @ H1)) by A2, A11, A9, A10, Th51;

        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 2( A15, A5);

      reconsider k as Nat;

      

       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 :: QC_LANG2:55

    

     Th55: H is_proper_subformula_of F implies ex G st G is_immediate_constituent_of F

    proof

      given 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 holds ex H1,F1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = F1 & H1 is_immediate_constituent_of F1;

      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 Nat;

      ((1 + 1) + k) = ((1 + k) + 1);

      then (1 + k) < n by A5, NAT_1: 13;

      then

      consider H1,F1 be Element of ( QC-WFF A) 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;

    theorem :: QC_LANG2:56

    

     Th56: 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_proper_subformula_of G and

       A2: G is_proper_subformula_of H;

      F is_subformula_of G by A1;

      then

      consider n, L such that

       A3: 1 <= n and

       A4: ( len L) = n and

       A5: (L . 1) = F and

       A6: (L . n) = G and

       A7: for k st 1 <= k & k < n holds ex H1,F1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = F1 & H1 is_immediate_constituent_of F1;

      1 < n by A1, 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;

      G is_subformula_of H by A2;

      then

      consider m, L9 such that

       A9: 1 <= m and

       A10: ( len L9) = m and

       A11: (L9 . 1) = G and

       A12: (L9 . m) = H and

       A13: for k st 1 <= k & k < m holds ex H1,F1 be Element of ( QC-WFF A) st (L9 . k) = H1 & (L9 . (k + 1)) = F1 & H1 is_immediate_constituent_of F1;

      reconsider k as Nat;

      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);

        

         A14: (((1 + k) + m) - (1 + k)) = m;

        m <= (m + (1 + k)) by NAT_1: 11;

        hence 1 <= l by A9, XXREAL_0: 2;

        ((1 + 1) + k) = ((1 + k) + 1);

        then

         A15: (1 + k) <= n by A8, NAT_1: 11;

        then

         A16: ( len L1) = (1 + k) by A4, FINSEQ_1: 17;

        hence

         A17: ( len K) = l by A10, FINSEQ_1: 22;

         A18:

        now

          let j be Nat;

          assume 1 <= j & j <= (1 + k);

          then

           A19: j in ( Seg (1 + k)) by FINSEQ_1: 1;

          then j in ( dom L1) by A4, A15, FINSEQ_1: 17;

          then (K . j) = (L1 . j) by FINSEQ_1:def 7;

          hence (K . j) = (L . j) by A19, FUNCT_1: 49;

        end;

        1 <= (1 + k) by NAT_1: 11;

        hence (K . 1) = F by A5, A18;

        (( len L1) + 1) <= (( len L1) + m) by A9, XREAL_1: 7;

        then ( len L1) < l by A16, NAT_1: 13;

        then (K . l) = (L9 . (l - ( len L1))) by A17, FINSEQ_1: 24;

        hence (K . l) = H by A4, A12, A15, A14, FINSEQ_1: 17;

        let j be Nat such that

         A20: 1 <= j and

         A21: j < l;

        (j + 0 ) <= (j + 1) by XREAL_1: 7;

        then

         A22: 1 <= (j + 1) by A20, XXREAL_0: 2;

         A23:

        now

          assume

           A24: j < (1 + k);

          then

           A25: (j + 1) <= (1 + k) by NAT_1: 13;

          then (j + 1) <= n by A15, XXREAL_0: 2;

          then j < n by NAT_1: 13;

          then

          consider F1,G1 be Element of ( QC-WFF A) such that

           A26: (L . j) = F1 & (L . (j + 1)) = G1 & F1 is_immediate_constituent_of G1 by A7, A20;

          take F1, G1;

          thus (K . j) = F1 & (K . (j + 1)) = G1 & F1 is_immediate_constituent_of G1 by A18, A20, A22, A24, A25, A26;

        end;

         A27:

        now

          

           A28: (j + 1) <= l by A21, NAT_1: 13;

          assume

           A29: (1 + k) < j;

          then

           A30: (1 + k) < (j + 1) by NAT_1: 13;

          ((1 + k) + 1) <= j by A29, NAT_1: 13;

          then

          consider j1 be Nat such that

           A31: j = (((1 + k) + 1) + j1) by NAT_1: 10;

          reconsider j1 as Nat;

          (j - (1 + k)) < (l - (1 + k)) by A21, XREAL_1: 9;

          then

          consider F1,G1 be Element of ( QC-WFF A) such that

           A32: (L9 . (1 + j1)) = F1 & (L9 . ((1 + j1) + 1)) = G1 & F1 is_immediate_constituent_of G1 by A13, A31, NAT_1: 11;

          take F1, G1;

          

           A33: (((1 + j1) + (1 + k)) - (1 + k)) = (((1 + j1) + (1 + k)) + ( - (1 + k)));

          ((j + 1) - ( len L1)) = (1 + (j + ( - ( len L1))))

          .= ((1 + j1) + 1) by A4, A15, A31, A33, FINSEQ_1: 17;

          hence (K . j) = F1 & (K . (j + 1)) = G1 & F1 is_immediate_constituent_of G1 by A16, A17, A21, A29, A30, A28, A33, A32, FINSEQ_1: 24;

        end;

        now

          

           A34: (j + 1) <= l & ((j + 1) - j) = ((j + 1) + ( - j)) by A21, NAT_1: 13;

          assume

           A35: j = (1 + k);

          then j < ((1 + k) + 1) by NAT_1: 13;

          then

          consider F1,G1 be Element of ( QC-WFF A) such that

           A36: (L . j) = F1 & (L . (j + 1)) = G1 & F1 is_immediate_constituent_of G1 by A7, A8, A20;

          take F1, G1;

          (1 + k) < (j + 1) by A35, NAT_1: 13;

          hence (K . j) = F1 & (K . (j + 1)) = G1 & F1 is_immediate_constituent_of G1 by A6, A11, A8, A16, A17, A18, A20, A35, A34, A36, FINSEQ_1: 24;

        end;

        hence thesis by A23, A27, XXREAL_0: 1;

      end;

      ( len ( @ F)) < ( len ( @ G)) by A1, Th54;

      hence thesis by A2, Th54;

    end;

    theorem :: QC_LANG2:57

    

     Th57: 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;

        now

          assume G <> H;

          then G is_proper_subformula_of H by A2;

          then F is_proper_subformula_of H by A3, Th56;

          hence thesis;

        end;

        hence thesis by A1;

      end;

      hence thesis by A2;

    end;

    theorem :: QC_LANG2:58

    

     Th58: 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;

      then

       A4: ( len ( @ G)) < ( len ( @ H)) by Th54;

      H is_proper_subformula_of G by A2, A3;

      hence contradiction by A4, Th54;

    end;

    theorem :: QC_LANG2:59

    

     Th59: not (G is_proper_subformula_of H & H is_subformula_of G) by Th58;

    theorem :: QC_LANG2:60

     not (G is_proper_subformula_of H & H is_proper_subformula_of G) by Th59;

    theorem :: QC_LANG2:61

    

     Th61: not (G is_subformula_of H & H is_immediate_constituent_of G) by Th53, Th59;

    theorem :: QC_LANG2:62

     not (G is_proper_subformula_of H & H is_immediate_constituent_of G) by Th53, Th59;

    theorem :: QC_LANG2:63

    

     Th63: F is_proper_subformula_of G & G is_subformula_of H or F is_subformula_of G & G is_proper_subformula_of H or F is_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_subformula_of H or F is_proper_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H

    proof

      assume

       A1: F is_proper_subformula_of G & G is_subformula_of H or F is_subformula_of G & G is_proper_subformula_of H or F is_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_subformula_of H or F is_proper_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_proper_subformula_of H;

      then F is_subformula_of G & G is_subformula_of H by Th52;

      hence F is_subformula_of H by Th57;

      thus thesis by A1, Th59, Th61;

    end;

    theorem :: QC_LANG2:64

    

     Th64: not F is_proper_subformula_of ( VERUM A)

    proof

      assume not thesis;

      then

      consider G such that

       A1: G is_immediate_constituent_of ( VERUM A) by Th55;

      thus thesis by A1, Th41;

    end;

    theorem :: QC_LANG2:65

    

     Th65: not F is_proper_subformula_of (P ! V)

    proof

      assume F is_proper_subformula_of (P ! V);

      then ex G st G is_immediate_constituent_of (P ! V) by Th55;

      hence contradiction by Th42;

    end;

    theorem :: QC_LANG2:66

    

     Th66: F is_subformula_of H iff F is_proper_subformula_of ( 'not' H)

    proof

      H is_immediate_constituent_of ( 'not' H);

      hence F is_subformula_of H implies F is_proper_subformula_of ( 'not' H) by Th63;

      given n, L such that

       A1: 1 <= n and

       A2: ( len L) = n and

       A3: (L . 1) = F and

       A4: (L . n) = ( 'not' H) and

       A5: for k st 1 <= k & k < n holds ex H1,F1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = F1 & H1 is_immediate_constituent_of F1;

      assume F <> ( 'not' H);

      then 1 < n by A1, A3, A4, XXREAL_0: 1;

      then (1 + 1) <= n by NAT_1: 13;

      then

      consider k be Nat such that

       A6: n = (2 + k) by NAT_1: 10;

      reconsider k as Nat;

      reconsider L1 = (L | ( Seg (1 + k))) as FinSequence by FINSEQ_1: 15;

      take m = (1 + k), L1;

      thus

       A7: 1 <= m by NAT_1: 11;

      (1 + k) <= ((1 + k) + 1) by NAT_1: 11;

      hence ( len L1) = m by A2, A6, FINSEQ_1: 17;

      

       A8: for j be Nat st 1 <= j <= m holds (L1 . j) = (L . j) by FUNCT_1: 49, FINSEQ_1: 1;

      hence (L1 . 1) = F by A3, A7;

      m < (m + 1) by NAT_1: 13;

      then

      consider F1,G1 be Element of ( QC-WFF A) such that

       A9: (L . m) = F1 and

       A10: (L . (m + 1)) = G1 & F1 is_immediate_constituent_of G1 by A5, A6, NAT_1: 11;

      F1 = H by A4, A6, A10, Th43;

      hence (L1 . m) = H by A7, A8, A9;

      let j be Nat;

      assume that

       A11: 1 <= j and

       A12: j < m;

      m <= (m + 1) by NAT_1: 11;

      then j < n by A6, A12, XXREAL_0: 2;

      then

      consider F1,G1 be Element of ( QC-WFF A) such that

       A13: (L . j) = F1 & (L . (j + 1)) = G1 & F1 is_immediate_constituent_of G1 by A5, A11;

      take F1, G1;

      1 <= (1 + j) & (j + 1) <= m by A11, A12, NAT_1: 13;

      hence thesis by A8, A11, A12, A13;

    end;

    theorem :: QC_LANG2:67

    ( 'not' F) is_subformula_of H implies F is_proper_subformula_of H

    proof

      F is_proper_subformula_of ( 'not' F) by Th66;

      hence thesis by Th63;

    end;

    theorem :: QC_LANG2:68

    F is_proper_subformula_of ( FALSUM A) iff F is_subformula_of ( VERUM A) by Th66;

    theorem :: QC_LANG2:69

    

     Th69: F is_subformula_of G or F is_subformula_of H iff F is_proper_subformula_of (G '&' H)

    proof

      G is_immediate_constituent_of (G '&' H) & H is_immediate_constituent_of (G '&' H);

      hence F is_subformula_of G or F is_subformula_of H implies F is_proper_subformula_of (G '&' H) by Th63;

      given n, L such that

       A1: 1 <= n and

       A2: ( len L) = n and

       A3: (L . 1) = F and

       A4: (L . n) = (G '&' H) and

       A5: for k st 1 <= k & k < n holds ex H1,F1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = F1 & H1 is_immediate_constituent_of F1;

      assume F <> (G '&' H);

      then 1 < n by A1, A3, A4, XXREAL_0: 1;

      then (1 + 1) <= n by NAT_1: 13;

      then

      consider k be Nat such that

       A6: n = (2 + k) by NAT_1: 10;

      reconsider k as Nat;

      ((1 + 1) + k) = ((1 + k) + 1);

      then (1 + k) < n by A6, NAT_1: 13;

      then

      consider H1,G1 be Element of ( QC-WFF A) such that

       A7: (L . (1 + k)) = H1 and

       A8: (L . ((1 + k) + 1)) = G1 & H1 is_immediate_constituent_of G1 by A5, 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

         A9: 1 <= m by NAT_1: 11;

        (1 + k) <= ((1 + k) + 1) by NAT_1: 11;

        hence ( len L1) = m by A2, A6, FINSEQ_1: 17;

        

         A10: for j be Nat st 1 <= j <= m holds (L1 . j) = (L . j) by FUNCT_1: 49, FINSEQ_1: 1;

        hence (L1 . 1) = F by A3, A9;

        thus (L1 . m) = H1 by A7, A9, A10;

        let j be Nat;

        assume that

         A11: 1 <= j and

         A12: j < m;

        m <= (m + 1) by NAT_1: 11;

        then j < n by A6, A12, XXREAL_0: 2;

        then

        consider F1,G1 be Element of ( QC-WFF A) such that

         A13: (L . j) = F1 & (L . (j + 1)) = G1 & F1 is_immediate_constituent_of G1 by A5, A11;

        take F1, G1;

        1 <= (1 + j) & (j + 1) <= m by A11, A12, NAT_1: 13;

        hence thesis by A10, A11, A12, A13;

      end;

      hence thesis by A4, A6, A8, Th45;

    end;

    theorem :: QC_LANG2:70

    (F '&' G) is_subformula_of H implies F is_proper_subformula_of H & G is_proper_subformula_of H

    proof

      F is_proper_subformula_of (F '&' G) & G is_proper_subformula_of (F '&' G) by Th69;

      hence thesis by Th63;

    end;

    theorem :: QC_LANG2:71

    

     Th71: F is_subformula_of H iff F is_proper_subformula_of ( All (x,H))

    proof

      H is_immediate_constituent_of ( All (x,H));

      hence F is_subformula_of H implies F is_proper_subformula_of ( All (x,H)) by Th63;

      given n, L such that

       A1: 1 <= n and

       A2: ( len L) = n and

       A3: (L . 1) = F and

       A4: (L . n) = ( All (x,H)) and

       A5: for k st 1 <= k & k < n holds ex H1,F1 be Element of ( QC-WFF A) st (L . k) = H1 & (L . (k + 1)) = F1 & H1 is_immediate_constituent_of F1;

      assume F <> ( All (x,H));

      then 1 < n by A1, A3, A4, XXREAL_0: 1;

      then (1 + 1) <= n by NAT_1: 13;

      then

      consider k be Nat such that

       A6: n = (2 + k) by NAT_1: 10;

      reconsider k as Nat;

      reconsider L1 = (L | ( Seg (1 + k))) as FinSequence by FINSEQ_1: 15;

      take m = (1 + k), L1;

      thus

       A7: 1 <= m by NAT_1: 11;

      (1 + k) <= ((1 + k) + 1) by NAT_1: 11;

      hence ( len L1) = m by A2, A6, FINSEQ_1: 17;

      

       A8: for j be Nat st 1 <= j <= m holds (L1 . j) = (L . j) by FUNCT_1: 49, FINSEQ_1: 1;

      hence (L1 . 1) = F by A3, A7;

      m < (m + 1) by NAT_1: 13;

      then

      consider F1,G1 be Element of ( QC-WFF A) such that

       A9: (L . m) = F1 and

       A10: (L . (m + 1)) = G1 & F1 is_immediate_constituent_of G1 by A5, A6, NAT_1: 11;

      F1 = H by A4, A6, A10, Th46;

      hence (L1 . m) = H by A7, A8, A9;

      let j be Nat;

      assume that

       A11: 1 <= j and

       A12: j < m;

      m <= (m + 1) by NAT_1: 11;

      then j < n by A6, A12, XXREAL_0: 2;

      then

      consider F1,G1 be Element of ( QC-WFF A) such that

       A13: (L . j) = F1 & (L . (j + 1)) = G1 & F1 is_immediate_constituent_of G1 by A5, A11;

      take F1, G1;

      1 <= (1 + j) & (j + 1) <= m by A11, A12, NAT_1: 13;

      hence thesis by A8, A11, A12, A13;

    end;

    theorem :: QC_LANG2:72

    ( All (x,H)) is_subformula_of F implies H is_proper_subformula_of F

    proof

      H is_proper_subformula_of ( All (x,H)) by Th71;

      hence thesis by Th63;

    end;

    theorem :: QC_LANG2:73

    (F '&' ( 'not' G)) is_proper_subformula_of (F => G) & F is_proper_subformula_of (F => G) & ( 'not' G) is_proper_subformula_of (F => G) & G is_proper_subformula_of (F => G)

    proof

      thus

       A1: (F '&' ( 'not' G)) is_proper_subformula_of (F => G) by Th66;

      F is_proper_subformula_of (F '&' ( 'not' G)) & ( 'not' G) is_proper_subformula_of (F '&' ( 'not' G)) by Th69;

      hence

       A2: F is_proper_subformula_of (F => G) & ( 'not' G) is_proper_subformula_of (F => G) by A1, Th56;

      G is_proper_subformula_of ( 'not' G) by Th66;

      hence thesis by A2, Th56;

    end;

    theorem :: QC_LANG2:74

    (( 'not' F) '&' ( 'not' G)) is_proper_subformula_of (F 'or' G) & ( 'not' F) is_proper_subformula_of (F 'or' G) & ( 'not' G) is_proper_subformula_of (F 'or' G) & F is_proper_subformula_of (F 'or' G) & G is_proper_subformula_of (F 'or' G)

    proof

      thus

       A1: (( 'not' F) '&' ( 'not' G)) is_proper_subformula_of (F 'or' G) by Th66;

      ( 'not' F) is_proper_subformula_of (( 'not' F) '&' ( 'not' G)) & ( 'not' G) is_proper_subformula_of (( 'not' F) '&' ( 'not' G)) by Th69;

      hence

       A2: ( 'not' F) is_proper_subformula_of (F 'or' G) & ( 'not' G) is_proper_subformula_of (F 'or' G) by A1, Th56;

      G is_proper_subformula_of ( 'not' G) & F is_proper_subformula_of ( 'not' F) by Th66;

      hence thesis by A2, Th56;

    end;

    theorem :: QC_LANG2:75

    H is atomic implies not F is_proper_subformula_of H by Th65;

    theorem :: QC_LANG2:76

    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 Th48;

      hence thesis by Th53;

    end;

    theorem :: QC_LANG2:77

    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 Th49;

      hence thesis by Th53;

    end;

    theorem :: QC_LANG2:78

    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 Th50;

      hence thesis by Th53;

    end;

    theorem :: QC_LANG2:79

    

     Th79: H is_subformula_of ( VERUM A) iff H = ( VERUM A) by Def21, Th64;

    theorem :: QC_LANG2:80

    

     Th80: H is_subformula_of (P ! V) iff H = (P ! V)

    proof

      thus H is_subformula_of (P ! V) implies H = (P ! V)

      proof

        assume

         A1: H is_subformula_of (P ! V);

        assume H <> (P ! V);

        then H is_proper_subformula_of (P ! V) by A1;

        then ex F st F is_immediate_constituent_of (P ! V) by Th55;

        hence contradiction by Th42;

      end;

      thus thesis;

    end;

    theorem :: QC_LANG2:81

    

     Th81: H is_subformula_of ( FALSUM A) iff H = ( FALSUM A) or H = ( VERUM A)

    proof

      thus H is_subformula_of ( FALSUM A) implies H = ( FALSUM A) or H = ( VERUM A)

      proof

        assume H is_subformula_of ( FALSUM A) & H <> ( FALSUM A);

        then H is_proper_subformula_of ( FALSUM A);

        then H is_subformula_of ( VERUM A) by Th66;

        hence thesis by Th79;

      end;

      ( VERUM A) is_immediate_constituent_of ( FALSUM A);

      then ( VERUM A) is_proper_subformula_of ( FALSUM A) by Th53;

      hence thesis;

    end;

    definition

      let A be QC-alphabet;

      let H be Element of ( QC-WFF A);

      :: QC_LANG2:def22

      func Subformulae H -> set means

      : Def22: for a be object holds a in it iff ex F be Element of ( QC-WFF A) st F = a & F is_subformula_of H;

      existence

      proof

        defpred P[ object] means ex F be Element of ( QC-WFF A) st F = $1 & F is_subformula_of H;

        consider X be set such that

         A1: for a be object holds a in X iff a in ( QC-WFF A) & P[a] from XBOOLE_0:sch 1;

        take X;

        let a be object;

        thus a in X implies ex F be Element of ( QC-WFF A) st F = a & F is_subformula_of H by A1;

        given F be Element of ( QC-WFF A) such that

         A2: F = a & F is_subformula_of H;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        defpred P[ object] means ex F be Element of ( QC-WFF A) st F = $1 & F is_subformula_of H;

        let X,Y be set such that

         A3: for a be object holds a in X iff P[a] and

         A4: for a be object holds a in Y iff P[a];

        thus thesis from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    theorem :: QC_LANG2:82

    

     Th82: 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 Def22;

      hence thesis;

    end;

    theorem :: QC_LANG2:83

    

     Th83: F is_subformula_of H implies ( Subformulae F) c= ( Subformulae H)

    proof

      assume

       A1: F is_subformula_of H;

      let a be object;

      assume a in ( Subformulae F);

      then

      consider F1 be Element of ( QC-WFF A) such that

       A2: F1 = a and

       A3: F1 is_subformula_of F by Def22;

      F1 is_subformula_of H by A1, A3, Th57;

      hence thesis by A2, Def22;

    end;

    theorem :: QC_LANG2:84

    G in ( Subformulae H) implies ( Subformulae G) c= ( Subformulae H) by Th82, Th83;

    theorem :: QC_LANG2:85

    

     Th85: ( Subformulae ( VERUM A)) = {( VERUM A)}

    proof

      thus ( Subformulae ( VERUM A)) c= {( VERUM A)}

      proof

        let a be object;

        assume a in ( Subformulae ( VERUM A));

        then

        consider F be Element of ( QC-WFF A) such that

         A1: F = a and

         A2: F is_subformula_of ( VERUM A) by Def22;

        F = ( VERUM A) by A2, Th79;

        hence thesis by A1, TARSKI:def 1;

      end;

      let a be object;

      assume a in {( VERUM A)};

      then a = ( VERUM A) by TARSKI:def 1;

      hence thesis by Def22;

    end;

    theorem :: QC_LANG2:86

    

     Th86: ( Subformulae (P ! V)) = {(P ! V)}

    proof

      thus ( Subformulae (P ! V)) c= {(P ! V)}

      proof

        let a be object;

        assume a in ( Subformulae (P ! V));

        then

        consider F such that

         A1: F = a and

         A2: F is_subformula_of (P ! V) by Def22;

        F = (P ! V) by A2, Th80;

        hence thesis by A1, TARSKI:def 1;

      end;

      let a be object;

      assume a in {(P ! V)};

      then a = (P ! V) by TARSKI:def 1;

      hence thesis by Def22;

    end;

    theorem :: QC_LANG2:87

    ( Subformulae ( FALSUM A)) = {( VERUM A), ( FALSUM A)}

    proof

      thus ( Subformulae ( FALSUM A)) c= {( VERUM A), ( FALSUM A)}

      proof

        let a be object;

        assume a in ( Subformulae ( FALSUM A));

        then ex F st F = a & F is_subformula_of ( FALSUM A) by Def22;

        then a = ( FALSUM A) or a = ( VERUM A) by Th81;

        hence thesis by TARSKI:def 2;

      end;

      let a be object;

      assume

       A1: a in {( VERUM A), ( FALSUM A)};

      then

       A2: a = ( VERUM A) or a = ( FALSUM A) by TARSKI:def 2;

      reconsider a as Element of ( QC-WFF A) by A1, TARSKI:def 2;

      a is_subformula_of ( FALSUM A) by A2, Th81;

      hence thesis by Def22;

    end;

    theorem :: QC_LANG2:88

    

     Th88: ( Subformulae ( 'not' H)) = (( Subformulae H) \/ {( 'not' H)})

    proof

      thus ( Subformulae ( 'not' H)) c= (( Subformulae H) \/ {( 'not' H)})

      proof

        let a be object;

        assume a in ( Subformulae ( 'not' H));

        then

        consider F such that

         A1: F = a and

         A2: F is_subformula_of ( 'not' H) by Def22;

        now

          assume F <> ( 'not' H);

          then F is_proper_subformula_of ( 'not' H) by A2;

          then F is_subformula_of H by Th66;

          hence a in ( Subformulae H) by A1, Def22;

        end;

        then a in ( Subformulae H) or a in {( 'not' H)} by A1, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let a be object such that

       A3: a in (( Subformulae H) \/ {( 'not' H)});

       A4:

      now

        assume a in ( Subformulae H);

        then

        consider F such that

         A5: F = a and

         A6: F is_subformula_of H by Def22;

        H is_immediate_constituent_of ( 'not' H);

        then H is_proper_subformula_of ( 'not' H) by Th53;

        then H is_subformula_of ( 'not' H);

        then F is_subformula_of ( 'not' H) by A6, Th57;

        hence thesis by A5, Def22;

      end;

      now

        assume a in {( 'not' H)};

        then a = ( 'not' H) by TARSKI:def 1;

        hence thesis by Def22;

      end;

      hence thesis by A3, A4, XBOOLE_0:def 3;

    end;

    theorem :: QC_LANG2:89

    

     Th89: ( Subformulae (H '&' F)) = ((( Subformulae H) \/ ( Subformulae F)) \/ {(H '&' F)})

    proof

      thus ( Subformulae (H '&' F)) c= ((( Subformulae H) \/ ( Subformulae F)) \/ {(H '&' F)})

      proof

        let a be object;

        assume a in ( Subformulae (H '&' F));

        then

        consider G such that

         A1: G = a and

         A2: G is_subformula_of (H '&' F) by Def22;

        now

          assume G <> (H '&' F);

          then G is_proper_subformula_of (H '&' F) by A2;

          then G is_subformula_of H or G is_subformula_of F by Th69;

          then a in ( Subformulae H) or a in ( Subformulae F) by A1, Def22;

          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 A1, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let a be object such that

       A3: a in ((( Subformulae H) \/ ( Subformulae F)) \/ {(H '&' F)});

       A4:

      now

        assume a in {(H '&' F)};

        then a = (H '&' F) by TARSKI:def 1;

        hence thesis by Def22;

      end;

       A5:

      now

        assume a in ( Subformulae F);

        then

        consider G such that

         A6: G = a and

         A7: G is_subformula_of F by Def22;

        F is_immediate_constituent_of (H '&' F);

        then F is_proper_subformula_of (H '&' F) by Th53;

        then F is_subformula_of (H '&' F);

        then G is_subformula_of (H '&' F) by A7, Th57;

        hence thesis by A6, Def22;

      end;

       A8:

      now

        assume a in ( Subformulae H);

        then

        consider G such that

         A9: G = a and

         A10: G is_subformula_of H by Def22;

        H is_immediate_constituent_of (H '&' F);

        then H is_proper_subformula_of (H '&' F) by Th53;

        then H is_subformula_of (H '&' F);

        then G is_subformula_of (H '&' F) by A10, Th57;

        hence thesis by A9, Def22;

      end;

      a in (( Subformulae H) \/ ( Subformulae F)) implies a in ( Subformulae H) or a in ( Subformulae F) by XBOOLE_0:def 3;

      hence thesis by A3, A8, A5, A4, XBOOLE_0:def 3;

    end;

    theorem :: QC_LANG2:90

    

     Th90: ( Subformulae ( All (x,H))) = (( Subformulae H) \/ {( All (x,H))})

    proof

      thus ( Subformulae ( All (x,H))) c= (( Subformulae H) \/ {( All (x,H))})

      proof

        let a be object;

        assume a in ( Subformulae ( All (x,H)));

        then

        consider F such that

         A1: F = a and

         A2: F is_subformula_of ( All (x,H)) by Def22;

        now

          assume F <> ( All (x,H));

          then F is_proper_subformula_of ( All (x,H)) by A2;

          then F is_subformula_of H by Th71;

          hence a in ( Subformulae H) by A1, Def22;

        end;

        then a in ( Subformulae H) or a in {( All (x,H))} by A1, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let a be object such that

       A3: a in (( Subformulae H) \/ {( All (x,H))});

       A4:

      now

        assume a in ( Subformulae H);

        then

        consider F such that

         A5: F = a and

         A6: F is_subformula_of H by Def22;

        H is_immediate_constituent_of ( All (x,H));

        then H is_proper_subformula_of ( All (x,H)) by Th53;

        then H is_subformula_of ( All (x,H));

        then F is_subformula_of ( All (x,H)) by A6, Th57;

        hence thesis by A5, Def22;

      end;

      now

        assume a in {( All (x,H))};

        then a = ( All (x,H)) by TARSKI:def 1;

        hence thesis by Def22;

      end;

      hence thesis by A3, A4, XBOOLE_0:def 3;

    end;

    theorem :: QC_LANG2:91

    

     Th91: ( Subformulae (F => G)) = ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)})

    proof

      

      thus ( Subformulae (F => G)) = (( Subformulae (F '&' ( 'not' G))) \/ {(F => G)}) by Th88

      .= (((( Subformulae F) \/ ( Subformulae ( 'not' G))) \/ {(F '&' ( 'not' G))}) \/ {(F => G)}) by Th89

      .= (((( Subformulae F) \/ (( Subformulae G) \/ {( 'not' G)})) \/ {(F '&' ( 'not' G))}) \/ {(F => G)}) by Th88

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G)}) \/ {(F '&' ( 'not' G))}) \/ {(F => G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G)}) \/ ( {(F '&' ( 'not' G))} \/ {(F => G)})) by XBOOLE_1: 4

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G)} \/ ( {(F '&' ( 'not' G))} \/ {(F => G)}))) by XBOOLE_1: 4

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G)} \/ {(F '&' ( 'not' G)), (F => G)})) by ENUMSET1: 1

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)}) by ENUMSET1: 2;

    end;

    theorem :: QC_LANG2:92

    ( Subformulae (F 'or' G)) = ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F), (( 'not' F) '&' ( 'not' G)), (F 'or' G)})

    proof

      

      thus ( Subformulae (F 'or' G)) = (( Subformulae (( 'not' F) '&' ( 'not' G))) \/ {(F 'or' G)}) by Th88

      .= (((( Subformulae ( 'not' F)) \/ ( Subformulae ( 'not' G))) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by Th89

      .= (((( Subformulae ( 'not' F)) \/ (( Subformulae G) \/ {( 'not' G)})) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by Th88

      .= ((((( Subformulae F) \/ {( 'not' F)}) \/ (( Subformulae G) \/ {( 'not' G)})) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by Th88

      .= (((( Subformulae F) \/ ((( Subformulae G) \/ {( 'not' G)}) \/ {( 'not' F)})) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ (( Subformulae G) \/ ( {( 'not' G)} \/ {( 'not' F)}))) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ (( Subformulae G) \/ {( 'not' G), ( 'not' F)})) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by ENUMSET1: 1

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F)}) \/ {(( 'not' F) '&' ( 'not' G))}) \/ {(F 'or' G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F)}) \/ ( {(( 'not' F) '&' ( 'not' G))} \/ {(F 'or' G)})) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F)}) \/ {(( 'not' F) '&' ( 'not' G)), (F 'or' G)}) by ENUMSET1: 1

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G), ( 'not' F)} \/ {(( 'not' F) '&' ( 'not' G)), (F 'or' G)})) by XBOOLE_1: 4

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), ( 'not' F), (( 'not' F) '&' ( 'not' G)), (F 'or' G)}) by ENUMSET1: 5;

    end;

    theorem :: QC_LANG2:93

    ( Subformulae (F <=> G)) = ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G), ( 'not' F), (G '&' ( 'not' F)), (G => F), (F <=> G)})

    proof

      

      thus ( Subformulae (F <=> G)) = ((( Subformulae (F => G)) \/ ( Subformulae (G => F))) \/ {(F <=> G)}) by Th89

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)}) \/ ( Subformulae (G => F))) \/ {(F <=> G)}) by Th91

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)}) \/ ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' F), (G '&' ( 'not' F)), (G => F)})) \/ {(F <=> G)}) by Th91

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G)}) \/ {( 'not' F), (G '&' ( 'not' F)), (G => F)})) \/ {(F <=> G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G), (F '&' ( 'not' G)), (F => G)} \/ {( 'not' F), (G '&' ( 'not' F)), (G => F)}))) \/ {(F <=> G)}) by XBOOLE_1: 4

      .= ((((( Subformulae F) \/ ( Subformulae G)) \/ (( Subformulae F) \/ ( Subformulae G))) \/ ( {( 'not' G), (F '&' ( 'not' G)), (F => G)} \/ {( 'not' F), (G '&' ( 'not' F)), (G => F)})) \/ {(F <=> G)}) by XBOOLE_1: 4

      .= (((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G), ( 'not' F), (G '&' ( 'not' F)), (G => F)}) \/ {(F <=> G)}) by ENUMSET1: 13

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ ( {( 'not' G), (F '&' ( 'not' G)), (F => G), ( 'not' F), (G '&' ( 'not' F)), (G => F)} \/ {(F <=> G)})) by XBOOLE_1: 4

      .= ((( Subformulae F) \/ ( Subformulae G)) \/ {( 'not' G), (F '&' ( 'not' G)), (F => G), ( 'not' F), (G '&' ( 'not' F)), (G => F), (F <=> G)}) by ENUMSET1: 21;

    end;

    theorem :: QC_LANG2:94

    H = ( VERUM A) or H is atomic iff ( Subformulae H) = {H}

    proof

      H is atomic implies ( Subformulae H) = {H} by Th86;

      hence H = ( VERUM A) or H is atomic implies ( Subformulae H) = {H} by Th85;

      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;

        then ( the_argument_of H) is_proper_subformula_of H by Th53;

        then ( the_argument_of H) is_subformula_of H;

        then

         A4: ( the_argument_of H) in ( Subformulae H) by Def22;

        ( len ( @ ( the_argument_of H))) <> ( len ( @ H)) by A3, Th51;

        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;

        then ( the_left_argument_of H) is_proper_subformula_of H by Th53;

        then ( the_left_argument_of H) is_subformula_of H;

        then

         A7: ( the_left_argument_of H) in ( Subformulae H) by Def22;

        ( len ( @ ( the_left_argument_of H))) <> ( len ( @ H)) by A6, Th51;

        hence contradiction by A1, A7, TARSKI:def 1;

      end;

      assume H <> ( VERUM A) & not H is atomic;

      then H is negative or H is conjunctive or H is universal by QC_LANG1: 9;

      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 Th3, Th6, QC_LANG1:def 24;

      then

       A8: ( the_scope_of H) is_immediate_constituent_of H by A2, A5;

      then ( the_scope_of H) is_proper_subformula_of H by Th53;

      then ( the_scope_of H) is_subformula_of H;

      then

       A9: ( the_scope_of H) in ( Subformulae H) by Def22;

      ( len ( @ ( the_scope_of H))) <> ( len ( @ H)) by A8, Th51;

      hence contradiction by A1, A9, TARSKI:def 1;

    end;

    theorem :: QC_LANG2:95

    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 QC_LANG1:def 24;

      hence thesis by Th88;

    end;

    theorem :: QC_LANG2:96

    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 Th3;

      hence thesis by Th89;

    end;

    theorem :: QC_LANG2:97

    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 Th6;

      hence thesis by Th90;

    end;

    theorem :: QC_LANG2:98

    (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, Th53;

      then

       A3: H is_subformula_of G;

      G is_subformula_of F by A2, Th82;

      then H is_subformula_of F by A3, Th57;

      hence thesis by Def22;

    end;