cqc_the2.miz



    begin

    reserve A for QC-alphabet;

    reserve X,T for Subset of ( CQC-WFF A);

    reserve F,G,H,p,q,r,t for Element of ( CQC-WFF A);

    reserve s,h for QC-formula of A;

    reserve x,y for bound_QC-variable of A;

    reserve f for FinSequence of [:( CQC-WFF A), Proof_Step_Kinds :];

    reserve i,j for Element of NAT ;

    theorem :: CQC_THE2:1

    

     Th1: (p => (q => r)) is valid implies ((p '&' q) => r) is valid

    proof

      

       A1: ((p => (q => r)) => ((p '&' q) => r)) in ( TAUT A) by PROCAL_1: 32;

      assume (p => (q => r)) in ( TAUT A);

      hence ((p '&' q) => r) in ( TAUT A) by A1, CQC_THE1: 46;

    end;

    theorem :: CQC_THE2:2

    

     Th2: (p => (q => r)) is valid implies ((q '&' p) => r) is valid

    proof

      assume (p => (q => r)) in ( TAUT A);

      then (p => (q => r)) is valid;

      then ((p '&' q) => r) is valid by Th1;

      then

       A1: ((p '&' q) => r) in ( TAUT A);

      ((q '&' p) => (p '&' q)) in ( TAUT A) by CQC_THE1: 45;

      hence ((q '&' p) => r) in ( TAUT A) by A1, LUKASI_1: 3;

    end;

    theorem :: CQC_THE2:3

    

     Th3: ((p '&' q) => r) is valid implies (p => (q => r)) is valid

    proof

      

       A1: (((p '&' q) => r) => (p => (q => r))) in ( TAUT A) by PROCAL_1: 31;

      assume ((p '&' q) => r) in ( TAUT A);

      hence (p => (q => r)) in ( TAUT A) by A1, CQC_THE1: 46;

    end;

    theorem :: CQC_THE2:4

    

     Th4: ((p '&' q) => r) is valid implies (q => (p => r)) is valid

    proof

      

       A1: ((q '&' p) => (p '&' q)) in ( TAUT A) by CQC_THE1: 45;

      assume ((p '&' q) => r) in ( TAUT A);

      then ((q '&' p) => r) in ( TAUT A) by A1, LUKASI_1: 3;

      then ((q '&' p) => r) is valid;

      then (q => (p => r)) is valid by Th3;

      hence (q => (p => r)) in ( TAUT A);

    end;

    

     Lm1: ((p '&' q) => p) is valid & ((p '&' q) => q) is valid by PROCAL_1: 19, PROCAL_1: 21;

    

     Lm2: (p '&' q) is valid implies p is valid & q is valid

    proof

      assume

       A1: (p '&' q) is valid;

      ((p '&' q) => p) is valid & ((p '&' q) => q) is valid by Lm1;

      hence thesis by A1, CQC_THE1: 65;

    end;

    

     Lm3: (p => q) is valid & (p => r) is valid implies (p => (q '&' r)) is valid by PROCAL_1: 52;

    

     Lm4: (p => q) is valid & (r => t) is valid implies ((p 'or' r) => (q 'or' t)) is valid by PROCAL_1: 57;

    

     Lm5: (p => q) is valid & (r => t) is valid implies ((p '&' r) => (q '&' t)) is valid by PROCAL_1: 56;

    

     Lm6: (p => (p 'or' q)) is valid & (p => (q 'or' p)) is valid by PROCAL_1: 3, PROCAL_1: 4;

    

     Lm7: (p => q) is valid & (r => q) is valid implies ((p 'or' r) => q) is valid by PROCAL_1: 53;

    

     Lm8: p is valid & q is valid implies (p '&' q) is valid by PROCAL_1: 47;

    

     Lm9: (p => q) is valid implies ((r '&' p) => (r '&' q)) is valid by PROCAL_1: 50;

    

     Lm10: (p => q) is valid implies ((p 'or' r) => (q 'or' r)) is valid by PROCAL_1: 48;

    

     Lm11: ((p 'or' q) => (( 'not' p) => q)) is valid by PROCAL_1: 5;

    

     Lm12: ((( 'not' p) => q) => (p 'or' q)) is valid

    proof

      (( 'not' ( 'not' p)) => p) in ( TAUT A) by LUKASI_1: 25;

      then ((( 'not' p) => q) => (( 'not' ( 'not' p)) 'or' q)) in ( TAUT A) & ((( 'not' ( 'not' p)) 'or' q) => (p 'or' q)) in ( TAUT A) by PROCAL_1: 14, PROCAL_1: 48;

      hence ((( 'not' p) => q) => (p 'or' q)) in ( TAUT A) by LUKASI_1: 3;

    end;

    

     Lm13: (p <=> p) is valid

    proof

      ((p => p) '&' (p => p)) is valid by Lm8;

      hence thesis by QC_LANG2:def 4;

    end;

    

     Lm14: (p => q) is valid & (q => p) is valid iff (p <=> q) is valid

    proof

      thus (p => q) is valid & (q => p) is valid implies (p <=> q) is valid

      proof

        assume (p => q) is valid & (q => p) is valid;

        then ((p => q) '&' (q => p)) is valid by Lm8;

        hence thesis by QC_LANG2:def 4;

      end;

      assume (p <=> q) is valid;

      then ((p => q) '&' (q => p)) is valid by QC_LANG2:def 4;

      hence thesis by Lm2;

    end;

    

     Lm15: (p <=> q) is valid implies (p is valid iff q is valid)

    proof

      assume

       A1: (p <=> q) in ( TAUT A);

      ((p <=> q) => (p => q)) in ( TAUT A) by PROCAL_1: 23;

      then

       A2: (p => q) in ( TAUT A) by A1, CQC_THE1: 46;

      thus p is valid implies q is valid by A2, CQC_THE1: 46;

      assume

       A3: q in ( TAUT A);

      ((p <=> q) => (q => p)) in ( TAUT A) by PROCAL_1: 24;

      then (q => p) in ( TAUT A) by A1, CQC_THE1: 46;

      hence p in ( TAUT A) by A3, CQC_THE1: 46;

    end;

    

     Lm16: (p => (q => r)) is valid & (r => t) is valid implies (p => (q => t)) is valid

    proof

      assume that

       A1: (p => (q => r)) is valid and

       A2: (r => t) is valid;

      ((p '&' q) => r) is valid by A1, Th1;

      then ((p '&' q) => t) is valid by A2, LUKASI_1: 42;

      hence thesis by Th3;

    end;

    theorem :: CQC_THE2:5

    

     Th5: y in ( still_not-bound_in ( All (x,s))) iff y in ( still_not-bound_in s) & y <> x

    proof

      ( still_not-bound_in ( All (x,s))) = (( still_not-bound_in s) \ {x}) by QC_LANG3: 12;

      hence thesis by ZFMISC_1: 56;

    end;

    theorem :: CQC_THE2:6

    

     Th6: y in ( still_not-bound_in ( Ex (x,s))) iff y in ( still_not-bound_in s) & y <> x

    proof

      ( still_not-bound_in ( Ex (x,s))) = (( still_not-bound_in s) \ {x}) by QC_LANG3: 19;

      hence thesis by ZFMISC_1: 56;

    end;

    theorem :: CQC_THE2:7

    

     Th7: y in ( still_not-bound_in (s => h)) iff y in ( still_not-bound_in s) or y in ( still_not-bound_in h)

    proof

      ( still_not-bound_in (s => h)) = (( still_not-bound_in s) \/ ( still_not-bound_in h)) by QC_LANG3: 16;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: CQC_THE2:8

    

     Th8: y in ( still_not-bound_in (s '&' h)) iff y in ( still_not-bound_in s) or y in ( still_not-bound_in h)

    proof

      ( still_not-bound_in (s '&' h)) = (( still_not-bound_in s) \/ ( still_not-bound_in h)) by QC_LANG3: 10;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: CQC_THE2:9

    

     Th9: y in ( still_not-bound_in (s 'or' h)) iff y in ( still_not-bound_in s) or y in ( still_not-bound_in h)

    proof

      ( still_not-bound_in (s 'or' h)) = (( still_not-bound_in s) \/ ( still_not-bound_in h)) by QC_LANG3: 14;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: CQC_THE2:10

     not x in ( still_not-bound_in ( All (x,y,s))) & not y in ( still_not-bound_in ( All (x,y,s)))

    proof

       not y in ( still_not-bound_in ( All (y,s))) by Th5;

      then

       A1: not y in ( still_not-bound_in ( All (x,( All (y,s))))) by Th5;

       not x in ( still_not-bound_in ( All (x,( All (y,s))))) by Th5;

      hence thesis by A1, QC_LANG2: 14;

    end;

    theorem :: CQC_THE2:11

     not x in ( still_not-bound_in ( Ex (x,y,s))) & not y in ( still_not-bound_in ( Ex (x,y,s)))

    proof

       not y in ( still_not-bound_in ( Ex (y,s))) by Th6;

      then

       A1: not y in ( still_not-bound_in ( Ex (x,( Ex (y,s))))) by Th6;

       not x in ( still_not-bound_in ( Ex (x,( Ex (y,s))))) by Th6;

      hence thesis by A1, QC_LANG2: 14;

    end;

    theorem :: CQC_THE2:12

    

     Th12: ((s => h) . x) = ((s . x) => (h . x))

    proof

      (s => h) = ( 'not' (s '&' ( 'not' h))) by QC_LANG2:def 2;

      

      hence ((s => h) . x) = ( 'not' ((s '&' ( 'not' h)) . x)) by CQC_LANG: 19

      .= ( 'not' ((s . x) '&' (( 'not' h) . x))) by CQC_LANG: 21

      .= ( 'not' ((s . x) '&' ( 'not' (h . x)))) by CQC_LANG: 19

      .= ((s . x) => (h . x)) by QC_LANG2:def 2;

    end;

    theorem :: CQC_THE2:13

    ((s 'or' h) . x) = ((s . x) 'or' (h . x))

    proof

      

      thus ((s 'or' h) . x) = (( 'not' (( 'not' s) '&' ( 'not' h))) . x) by QC_LANG2:def 3

      .= ( 'not' ((( 'not' s) '&' ( 'not' h)) . x)) by CQC_LANG: 19

      .= ( 'not' ((( 'not' s) . x) '&' (( 'not' h) . x))) by CQC_LANG: 21

      .= ( 'not' (( 'not' (s . x)) '&' (( 'not' h) . x))) by CQC_LANG: 19

      .= ( 'not' (( 'not' (s . x)) '&' ( 'not' (h . x)))) by CQC_LANG: 19

      .= ((s . x) 'or' (h . x)) by QC_LANG2:def 3;

    end;

    theorem :: CQC_THE2:14

    x <> y implies (( Ex (x,p)) . y) = ( Ex (x,(p . y)))

    proof

      assume

       A1: x <> y;

      

      thus (( Ex (x,p)) . y) = (( 'not' ( All (x,( 'not' p)))) . y) by QC_LANG2:def 5

      .= ( 'not' (( All (x,( 'not' p))) . y)) by CQC_LANG: 19

      .= ( 'not' ( All (x,(( 'not' p) . y)))) by A1, CQC_LANG: 25

      .= ( 'not' ( All (x,( 'not' (p . y))))) by CQC_LANG: 19

      .= ( Ex (x,(p . y))) by QC_LANG2:def 5;

    end;

    theorem :: CQC_THE2:15

    

     Th15: (p => ( Ex (x,p))) is valid

    proof

      (( All (x,( 'not' p))) => ( 'not' p)) is valid by CQC_THE1: 66;

      then (( 'not' ( 'not' p)) => ( 'not' ( All (x,( 'not' p))))) is valid by LUKASI_1: 52;

      then

       A1: (( 'not' ( 'not' p)) => ( Ex (x,p))) is valid by QC_LANG2:def 5;

      ((( 'not' ( 'not' p)) => ( Ex (x,p))) => (p => ( Ex (x,p)))) is valid;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:16

    

     Th16: p is valid implies ( Ex (x,p)) is valid

    proof

      assume

       A1: p is valid;

      (p => ( Ex (x,p))) is valid by Th15;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:17

    (( All (x,p)) => ( Ex (x,p))) is valid

    proof

      (( All (x,p)) => p) is valid & (p => ( Ex (x,p))) is valid by Th15, CQC_THE1: 66;

      hence thesis by LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:18

    (( All (x,p)) => ( Ex (y,p))) is valid

    proof

      (( All (x,p)) => p) is valid & (p => ( Ex (y,p))) is valid by Th15, CQC_THE1: 66;

      hence thesis by LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:19

    

     Th19: (p => q) is valid & not x in ( still_not-bound_in q) implies (( Ex (x,p)) => q) is valid

    proof

      assume (p => q) is valid & not x in ( still_not-bound_in q);

      then (( 'not' q) => ( 'not' p)) is valid & not x in ( still_not-bound_in ( 'not' q)) by LUKASI_1: 52, QC_LANG3: 7;

      then (( 'not' q) => ( All (x,( 'not' p)))) is valid by CQC_THE1: 67;

      then (( 'not' ( All (x,( 'not' p)))) => ( 'not' ( 'not' q))) is valid by LUKASI_1: 52;

      then (( Ex (x,p)) => ( 'not' ( 'not' q))) is valid by QC_LANG2:def 5;

      hence thesis by LUKASI_1: 55;

    end;

    theorem :: CQC_THE2:20

    

     Th20: not x in ( still_not-bound_in p) implies (( Ex (x,p)) => p) is valid

    proof

      

       A1: (p => p) is valid;

      assume not x in ( still_not-bound_in p);

      hence thesis by A1, Th19;

    end;

    theorem :: CQC_THE2:21

     not x in ( still_not-bound_in p) & ( Ex (x,p)) is valid implies p is valid

    proof

      assume that

       A1: not x in ( still_not-bound_in p) and

       A2: ( Ex (x,p)) is valid;

      (( Ex (x,p)) => p) is valid by A1, Th20;

      hence thesis by A2, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:22

    

     Th22: p = (h . x) & q = (h . y) & not y in ( still_not-bound_in h) implies (p => ( Ex (y,q))) is valid

    proof

      assume that

       A1: p = (h . x) and

       A2: q = (h . y) and

       A3: not y in ( still_not-bound_in h);

      

       A4: ((h => ( Ex (y,q))) . x) = ((h . x) => (( Ex (y,q)) . x)) by Th12

      .= (p => ( Ex (y,q))) by A1, CQC_LANG: 27;

       not y in ( still_not-bound_in ( Ex (y,q))) by Th6;

      then

       A5: not y in ( still_not-bound_in (h => ( Ex (y,q)))) by A3, Th7;

      

       A6: (q => ( Ex (y,q))) is valid by Th15;

      ((h => ( Ex (y,q))) . y) = ((h . y) => (( Ex (y,q)) . y)) by Th12

      .= (q => ( Ex (y,q))) by A2, CQC_LANG: 27;

      hence thesis by A6, A4, A5, CQC_THE1: 68;

    end;

    theorem :: CQC_THE2:23

    

     Th23: p is valid implies ( All (x,p)) is valid

    proof

      

       A1: (p => ((( All (x,p)) => ( All (x,p))) => p)) is valid;

       not x in ( still_not-bound_in ( All (x,p))) by Th5;

      then

       A2: not x in ( still_not-bound_in (( All (x,p)) => ( All (x,p)))) by Th7;

      assume p is valid;

      then ((( All (x,p)) => ( All (x,p))) => p) is valid by A1, CQC_THE1: 65;

      then ((( All (x,p)) => ( All (x,p))) => ( All (x,p))) is valid by A2, CQC_THE1: 67;

      hence thesis by CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:24

    

     Th24: not x in ( still_not-bound_in p) implies (p => ( All (x,p))) is valid

    proof

      

       A1: (p => p) is valid;

      assume not x in ( still_not-bound_in p);

      hence thesis by A1, CQC_THE1: 67;

    end;

    theorem :: CQC_THE2:25

    

     Th25: p = (h . x) & q = (h . y) & not x in ( still_not-bound_in h) implies (( All (x,p)) => q) is valid

    proof

      assume that

       A1: p = (h . x) and

       A2: q = (h . y) and

       A3: not x in ( still_not-bound_in h);

      

       A4: ((( All (x,p)) => h) . y) = ((( All (x,p)) . y) => q) by A2, Th12

      .= (( All (x,p)) => q) by CQC_LANG: 27;

       not x in ( still_not-bound_in ( All (x,p))) by Th5;

      then

       A5: (( All (x,p)) => p) is valid & not x in ( still_not-bound_in (( All (x,p)) => h)) by A3, Th7, CQC_THE1: 66;

      ((( All (x,p)) => h) . x) = ((( All (x,p)) . x) => p) by A1, Th12

      .= (( All (x,p)) => p) by CQC_LANG: 27;

      hence thesis by A4, A5, CQC_THE1: 68;

    end;

    theorem :: CQC_THE2:26

     not y in ( still_not-bound_in p) implies (( All (x,p)) => ( All (y,p))) is valid

    proof

      assume not y in ( still_not-bound_in p);

      then (( All (x,p)) => p) is valid & not y in ( still_not-bound_in ( All (x,p))) by Th5, CQC_THE1: 66;

      hence thesis by CQC_THE1: 67;

    end;

    theorem :: CQC_THE2:27

    p = (h . x) & q = (h . y) & not x in ( still_not-bound_in h) & not y in ( still_not-bound_in p) implies (( All (x,p)) => ( All (y,q))) is valid

    proof

      assume p = (h . x) & q = (h . y) & not x in ( still_not-bound_in h) & not y in ( still_not-bound_in p);

      then ( not y in ( still_not-bound_in ( All (x,p)))) & (( All (x,p)) => q) is valid by Th5, Th25;

      hence thesis by CQC_THE1: 67;

    end;

    theorem :: CQC_THE2:28

     not x in ( still_not-bound_in p) implies (( Ex (x,p)) => ( Ex (y,p))) is valid

    proof

      assume not x in ( still_not-bound_in p);

      then

       A1: not x in ( still_not-bound_in ( Ex (y,p))) by Th6;

      (p => ( Ex (y,p))) is valid by Th15;

      hence thesis by A1, Th19;

    end;

    theorem :: CQC_THE2:29

    p = (h . x) & q = (h . y) & not x in ( still_not-bound_in q) & not y in ( still_not-bound_in h) implies (( Ex (x,p)) => ( Ex (y,q))) is valid

    proof

      assume p = (h . x) & q = (h . y) & not x in ( still_not-bound_in q) & not y in ( still_not-bound_in h);

      then ( not x in ( still_not-bound_in ( Ex (y,q)))) & (p => ( Ex (y,q))) is valid by Th6, Th22;

      hence thesis by Th19;

    end;

    theorem :: CQC_THE2:30

    

     Th30: (( All (x,(p => q))) => (( All (x,p)) => ( All (x,q)))) is valid

    proof

      (( All (x,(p => q))) => (p => q)) is valid by CQC_THE1: 66;

      then

       A1: (p => (( All (x,(p => q))) => q)) is valid by LUKASI_1: 44;

      (( All (x,p)) => p) is valid by CQC_THE1: 66;

      then (( All (x,p)) => (( All (x,(p => q))) => q)) is valid by A1, LUKASI_1: 42;

      then

       A2: ((( All (x,(p => q))) '&' ( All (x,p))) => q) is valid by Th2;

      ( not x in ( still_not-bound_in ( All (x,(p => q))))) & not x in ( still_not-bound_in ( All (x,p))) by Th5;

      then not x in ( still_not-bound_in (( All (x,(p => q))) '&' ( All (x,p)))) by Th8;

      then ((( All (x,(p => q))) '&' ( All (x,p))) => ( All (x,q))) is valid by A2, CQC_THE1: 67;

      hence thesis by Th3;

    end;

    theorem :: CQC_THE2:31

    

     Th31: ( All (x,(p => q))) is valid implies (( All (x,p)) => ( All (x,q))) is valid

    proof

      assume

       A1: ( All (x,(p => q))) is valid;

      (( All (x,(p => q))) => (( All (x,p)) => ( All (x,q)))) is valid by Th30;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:32

    

     Th32: (( All (x,(p <=> q))) => (( All (x,p)) <=> ( All (x,q)))) is valid

    proof

      

       A1: (( All (x,((p => q) '&' (q => p)))) => ((p => q) '&' (q => p))) is valid by CQC_THE1: 66;

      ((p <=> q) => (p <=> q)) is valid;

      then ((p <=> q) => ((p => q) '&' (q => p))) is valid by QC_LANG2:def 4;

      then ( All (x,((p <=> q) => ((p => q) '&' (q => p))))) is valid by Th23;

      then

       A2: (( All (x,(p <=> q))) => ( All (x,((p => q) '&' (q => p))))) is valid by Th31;

      (( All (x,(p => q))) => (( All (x,p)) => ( All (x,q)))) is valid & (( All (x,(q => p))) => (( All (x,q)) => ( All (x,p)))) is valid by Th30;

      then ((( All (x,(p => q))) '&' ( All (x,(q => p)))) => ((( All (x,p)) => ( All (x,q))) '&' (( All (x,q)) => ( All (x,p))))) is valid by Lm5;

      then

       A3: ((( All (x,(p => q))) '&' ( All (x,(q => p)))) => (( All (x,p)) <=> ( All (x,q)))) is valid by QC_LANG2:def 4;

      

       A4: not x in ( still_not-bound_in ( All (x,((p => q) '&' (q => p))))) by Th5;

      (((p => q) '&' (q => p)) => (q => p)) is valid by Lm1;

      then (( All (x,((p => q) '&' (q => p)))) => (q => p)) is valid by A1, LUKASI_1: 42;

      then

       A5: (( All (x,((p => q) '&' (q => p)))) => ( All (x,(q => p)))) is valid by A4, CQC_THE1: 67;

      (((p => q) '&' (q => p)) => (p => q)) is valid by Lm1;

      then (( All (x,((p => q) '&' (q => p)))) => (p => q)) is valid by A1, LUKASI_1: 42;

      then (( All (x,((p => q) '&' (q => p)))) => ( All (x,(p => q)))) is valid by A4, CQC_THE1: 67;

      then (( All (x,((p => q) '&' (q => p)))) => (( All (x,(p => q))) '&' ( All (x,(q => p))))) is valid by A5, Lm3;

      then (( All (x,((p => q) '&' (q => p)))) => (( All (x,p)) <=> ( All (x,q)))) is valid by A3, LUKASI_1: 42;

      hence thesis by A2, LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:33

    ( All (x,(p <=> q))) is valid implies (( All (x,p)) <=> ( All (x,q))) is valid

    proof

      assume

       A1: ( All (x,(p <=> q))) is valid;

      (( All (x,(p <=> q))) => (( All (x,p)) <=> ( All (x,q)))) is valid by Th32;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:34

    

     Th34: (( All (x,(p => q))) => (( Ex (x,p)) => ( Ex (x,q)))) is valid

    proof

      (( All (x,(p => q))) => (p => q)) is valid by CQC_THE1: 66;

      then

       A1: ((p '&' ( All (x,(p => q)))) => q) is valid by Th2;

      (q => ( Ex (x,q))) is valid by Th15;

      then ((p '&' ( All (x,(p => q)))) => ( Ex (x,q))) is valid by A1, LUKASI_1: 42;

      then

       A2: (p => (( All (x,(p => q))) => ( Ex (x,q)))) is valid by Th3;

      ( not x in ( still_not-bound_in ( All (x,(p => q))))) & not x in ( still_not-bound_in ( Ex (x,q))) by Th5, Th6;

      then not x in ( still_not-bound_in (( All (x,(p => q))) => ( Ex (x,q)))) by Th7;

      then (( Ex (x,p)) => (( All (x,(p => q))) => ( Ex (x,q)))) is valid by A2, Th19;

      hence thesis by LUKASI_1: 44;

    end;

    theorem :: CQC_THE2:35

    

     Th35: ( All (x,(p => q))) is valid implies (( Ex (x,p)) => ( Ex (x,q))) is valid

    proof

      assume

       A1: ( All (x,(p => q))) is valid;

      (( All (x,(p => q))) => (( Ex (x,p)) => ( Ex (x,q)))) is valid by Th34;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:36

    

     Th36: (( All (x,(p '&' q))) => (( All (x,p)) '&' ( All (x,q)))) is valid & ((( All (x,p)) '&' ( All (x,q))) => ( All (x,(p '&' q)))) is valid

    proof

      (( All (x,p)) => p) is valid & (( All (x,q)) => q) is valid by CQC_THE1: 66;

      then

       A1: ((( All (x,p)) '&' ( All (x,q))) => (p '&' q)) is valid by Lm5;

      ( All (x,((p '&' q) => q))) is valid & (( All (x,((p '&' q) => q))) => (( All (x,(p '&' q))) => ( All (x,q)))) is valid by Lm1, Th23, Th30;

      then

       A2: (( All (x,(p '&' q))) => ( All (x,q))) is valid by CQC_THE1: 65;

      ( All (x,((p '&' q) => p))) is valid & (( All (x,((p '&' q) => p))) => (( All (x,(p '&' q))) => ( All (x,p)))) is valid by Lm1, Th23, Th30;

      then (( All (x,(p '&' q))) => ( All (x,p))) is valid by CQC_THE1: 65;

      hence (( All (x,(p '&' q))) => (( All (x,p)) '&' ( All (x,q)))) is valid by A2, Lm3;

      ( not x in ( still_not-bound_in ( All (x,p)))) & not x in ( still_not-bound_in ( All (x,q))) by Th5;

      then not x in ( still_not-bound_in (( All (x,p)) '&' ( All (x,q)))) by Th8;

      hence thesis by A1, CQC_THE1: 67;

    end;

    theorem :: CQC_THE2:37

    

     Th37: (( All (x,(p '&' q))) <=> (( All (x,p)) '&' ( All (x,q)))) is valid

    proof

      (( All (x,(p '&' q))) => (( All (x,p)) '&' ( All (x,q)))) is valid & ((( All (x,p)) '&' ( All (x,q))) => ( All (x,(p '&' q)))) is valid by Th36;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:38

    ( All (x,(p '&' q))) is valid iff (( All (x,p)) '&' ( All (x,q))) is valid

    proof

      (( All (x,(p '&' q))) <=> (( All (x,p)) '&' ( All (x,q)))) is valid by Th37;

      hence thesis by Lm15;

    end;

    theorem :: CQC_THE2:39

    

     Th39: ((( All (x,p)) 'or' ( All (x,q))) => ( All (x,(p 'or' q)))) is valid

    proof

      ( All (x,(q => (p 'or' q)))) is valid & (( All (x,(q => (p 'or' q)))) => (( All (x,q)) => ( All (x,(p 'or' q))))) is valid by Lm6, Th23, Th30;

      then

       A1: (( All (x,q)) => ( All (x,(p 'or' q)))) is valid by CQC_THE1: 65;

      ( All (x,(p => (p 'or' q)))) is valid & (( All (x,(p => (p 'or' q)))) => (( All (x,p)) => ( All (x,(p 'or' q))))) is valid by Lm6, Th23, Th30;

      then (( All (x,p)) => ( All (x,(p 'or' q)))) is valid by CQC_THE1: 65;

      hence thesis by A1, Lm7;

    end;

    theorem :: CQC_THE2:40

    

     Th40: (( Ex (x,(p 'or' q))) => (( Ex (x,p)) 'or' ( Ex (x,q)))) is valid & ((( Ex (x,p)) 'or' ( Ex (x,q))) => ( Ex (x,(p 'or' q)))) is valid

    proof

      ( not x in ( still_not-bound_in ( Ex (x,p)))) & not x in ( still_not-bound_in ( Ex (x,q))) by Th6;

      then

       A1: not x in ( still_not-bound_in (( Ex (x,p)) 'or' ( Ex (x,q)))) by Th9;

      (p => ( Ex (x,p))) is valid & (q => ( Ex (x,q))) is valid by Th15;

      then ((p 'or' q) => (( Ex (x,p)) 'or' ( Ex (x,q)))) is valid by Lm4;

      hence (( Ex (x,(p 'or' q))) => (( Ex (x,p)) 'or' ( Ex (x,q)))) is valid by A1, Th19;

      ( All (x,(q => (p 'or' q)))) is valid & (( All (x,(q => (p 'or' q)))) => (( Ex (x,q)) => ( Ex (x,(p 'or' q))))) is valid by Lm6, Th23, Th34;

      then

       A2: (( Ex (x,q)) => ( Ex (x,(p 'or' q)))) is valid by CQC_THE1: 65;

      ( All (x,(p => (p 'or' q)))) is valid & (( All (x,(p => (p 'or' q)))) => (( Ex (x,p)) => ( Ex (x,(p 'or' q))))) is valid by Lm6, Th23, Th34;

      then (( Ex (x,p)) => ( Ex (x,(p 'or' q)))) is valid by CQC_THE1: 65;

      hence thesis by A2, Lm7;

    end;

    theorem :: CQC_THE2:41

    

     Th41: (( Ex (x,(p 'or' q))) <=> (( Ex (x,p)) 'or' ( Ex (x,q)))) is valid

    proof

      (( Ex (x,(p 'or' q))) => (( Ex (x,p)) 'or' ( Ex (x,q)))) is valid & ((( Ex (x,p)) 'or' ( Ex (x,q))) => ( Ex (x,(p 'or' q)))) is valid by Th40;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:42

    ( Ex (x,(p 'or' q))) is valid iff (( Ex (x,p)) 'or' ( Ex (x,q))) is valid

    proof

      (( Ex (x,(p 'or' q))) <=> (( Ex (x,p)) 'or' ( Ex (x,q)))) is valid by Th41;

      hence thesis by Lm15;

    end;

    theorem :: CQC_THE2:43

    

     Th43: (( Ex (x,(p '&' q))) => (( Ex (x,p)) '&' ( Ex (x,q)))) is valid

    proof

      ( All (x,((p '&' q) => q))) is valid by Lm1, Th23;

      then

       A1: (( Ex (x,(p '&' q))) => ( Ex (x,q))) is valid by Th35;

      ( All (x,((p '&' q) => p))) is valid by Lm1, Th23;

      then (( Ex (x,(p '&' q))) => ( Ex (x,p))) is valid by Th35;

      hence thesis by A1, Lm3;

    end;

    theorem :: CQC_THE2:44

    ( Ex (x,(p '&' q))) is valid implies (( Ex (x,p)) '&' ( Ex (x,q))) is valid

    proof

      assume

       A1: ( Ex (x,(p '&' q))) is valid;

      (( Ex (x,(p '&' q))) => (( Ex (x,p)) '&' ( Ex (x,q)))) is valid by Th43;

      hence thesis by A1, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:45

    

     Th45: (( All (x,( 'not' ( 'not' p)))) => ( All (x,p))) is valid & (( All (x,p)) => ( All (x,( 'not' ( 'not' p))))) is valid

    proof

      ( All (x,(( 'not' ( 'not' p)) => p))) is valid & ( All (x,(p => ( 'not' ( 'not' p))))) is valid by Th23;

      hence thesis by Th31;

    end;

    theorem :: CQC_THE2:46

    (( All (x,( 'not' ( 'not' p)))) <=> ( All (x,p))) is valid

    proof

      (( All (x,( 'not' ( 'not' p)))) => ( All (x,p))) is valid & (( All (x,p)) => ( All (x,( 'not' ( 'not' p))))) is valid by Th45;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:47

    

     Th47: (( Ex (x,( 'not' ( 'not' p)))) => ( Ex (x,p))) is valid & (( Ex (x,p)) => ( Ex (x,( 'not' ( 'not' p))))) is valid

    proof

      ( All (x,(( 'not' ( 'not' p)) => p))) is valid & ( All (x,(p => ( 'not' ( 'not' p))))) is valid by Th23;

      hence thesis by Th35;

    end;

    theorem :: CQC_THE2:48

    (( Ex (x,( 'not' ( 'not' p)))) <=> ( Ex (x,p))) is valid

    proof

      (( Ex (x,( 'not' ( 'not' p)))) => ( Ex (x,p))) is valid & (( Ex (x,p)) => ( Ex (x,( 'not' ( 'not' p))))) is valid by Th47;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:49

    

     Th49: (( 'not' ( Ex (x,( 'not' p)))) => ( All (x,p))) is valid & (( All (x,p)) => ( 'not' ( Ex (x,( 'not' p))))) is valid

    proof

      

       A1: (( All (x,( 'not' ( 'not' p)))) => ( All (x,p))) is valid by Th45;

      

       A2: ( 'not' ( Ex (x,( 'not' p)))) = ( 'not' ( 'not' ( All (x,( 'not' ( 'not' p)))))) by QC_LANG2:def 5;

      then (( 'not' ( Ex (x,( 'not' p)))) => ( All (x,( 'not' ( 'not' p))))) is valid;

      hence (( 'not' ( Ex (x,( 'not' p)))) => ( All (x,p))) is valid by A1, LUKASI_1: 42;

      (( All (x,p)) => ( All (x,( 'not' ( 'not' p))))) is valid & (( All (x,( 'not' ( 'not' p)))) => ( 'not' ( 'not' ( All (x,( 'not' ( 'not' p))))))) is valid by Th45;

      hence thesis by A2, LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:50

    (( 'not' ( Ex (x,( 'not' p)))) <=> ( All (x,p))) is valid

    proof

      (( 'not' ( Ex (x,( 'not' p)))) => ( All (x,p))) is valid & (( All (x,p)) => ( 'not' ( Ex (x,( 'not' p))))) is valid by Th49;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:51

    

     Th51: (( 'not' ( All (x,p))) => ( Ex (x,( 'not' p)))) is valid & (( Ex (x,( 'not' p))) => ( 'not' ( All (x,p)))) is valid

    proof

      

       A1: ( Ex (x,( 'not' p))) = ( 'not' ( All (x,( 'not' ( 'not' p))))) by QC_LANG2:def 5;

      (( All (x,( 'not' ( 'not' p)))) => ( All (x,p))) is valid by Th45;

      hence (( 'not' ( All (x,p))) => ( Ex (x,( 'not' p)))) is valid by A1, LUKASI_1: 52;

      (( All (x,p)) => ( All (x,( 'not' ( 'not' p))))) is valid by Th45;

      hence thesis by A1, LUKASI_1: 52;

    end;

    theorem :: CQC_THE2:52

    (( 'not' ( All (x,p))) <=> ( Ex (x,( 'not' p)))) is valid

    proof

      (( 'not' ( All (x,p))) => ( Ex (x,( 'not' p)))) is valid & (( Ex (x,( 'not' p))) => ( 'not' ( All (x,p)))) is valid by Th51;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:53

    (( 'not' ( Ex (x,p))) => ( All (x,( 'not' p)))) is valid & (( All (x,( 'not' p))) => ( 'not' ( Ex (x,p)))) is valid

    proof

      

       A1: ( 'not' ( Ex (x,p))) = ( 'not' ( 'not' ( All (x,( 'not' p))))) by QC_LANG2:def 5;

      hence (( 'not' ( Ex (x,p))) => ( All (x,( 'not' p)))) is valid;

      thus thesis by A1;

    end;

    theorem :: CQC_THE2:54

    

     Th54: (( All (x,( 'not' p))) <=> ( 'not' ( Ex (x,p)))) is valid

    proof

      (( 'not' ( 'not' ( All (x,( 'not' p))))) => ( All (x,( 'not' p)))) is valid;

      then

       A1: (( 'not' ( Ex (x,p))) => ( All (x,( 'not' p)))) is valid by QC_LANG2:def 5;

      (( All (x,( 'not' p))) => ( 'not' ( 'not' ( All (x,( 'not' p)))))) is valid;

      then (( All (x,( 'not' p))) => ( 'not' ( Ex (x,p)))) is valid by QC_LANG2:def 5;

      hence thesis by A1, Lm14;

    end;

    theorem :: CQC_THE2:55

    (( All (x,( All (y,p)))) => ( All (y,( All (x,p))))) is valid & (( All (x,y,p)) => ( All (y,x,p))) is valid

    proof

       not y in ( still_not-bound_in ( All (y,p))) by Th5;

      then

       A1: not y in ( still_not-bound_in ( All (x,( All (y,p))))) by Th5;

      ( All (x,(( All (y,p)) => p))) is valid & (( All (x,(( All (y,p)) => p))) => (( All (x,( All (y,p)))) => ( All (x,p)))) is valid by Th23, Th30, CQC_THE1: 66;

      then (( All (x,( All (y,p)))) => ( All (x,p))) is valid by CQC_THE1: 65;

      hence (( All (x,( All (y,p)))) => ( All (y,( All (x,p))))) is valid by A1, CQC_THE1: 67;

      then (( All (x,y,p)) => ( All (y,( All (x,p))))) is valid by QC_LANG2: 14;

      hence thesis by QC_LANG2: 14;

    end;

    theorem :: CQC_THE2:56

    p = (h . x) & q = (h . y) & not y in ( still_not-bound_in h) implies (( All (x,( All (y,q)))) => ( All (x,p))) is valid

    proof

      assume p = (h . x) & q = (h . y) & not y in ( still_not-bound_in h);

      then ( All (x,(( All (y,q)) => p))) is valid by Th23, Th25;

      hence thesis by Th31;

    end;

    theorem :: CQC_THE2:57

    (( Ex (x,( Ex (y,p)))) => ( Ex (y,( Ex (x,p))))) is valid & (( Ex (x,y,p)) => ( Ex (y,x,p))) is valid

    proof

       not x in ( still_not-bound_in ( Ex (x,p))) by Th6;

      then

       A1: not x in ( still_not-bound_in ( Ex (y,( Ex (x,p))))) by Th6;

      ( All (y,(p => ( Ex (x,p))))) is valid & (( All (y,(p => ( Ex (x,p))))) => (( Ex (y,p)) => ( Ex (y,( Ex (x,p)))))) is valid by Th15, Th23, Th34;

      then (( Ex (y,p)) => ( Ex (y,( Ex (x,p))))) is valid by CQC_THE1: 65;

      hence (( Ex (x,( Ex (y,p)))) => ( Ex (y,( Ex (x,p))))) is valid by A1, Th19;

      then (( Ex (x,y,p)) => ( Ex (y,( Ex (x,p))))) is valid by QC_LANG2: 14;

      hence thesis by QC_LANG2: 14;

    end;

    theorem :: CQC_THE2:58

    p = (h . x) & q = (h . y) & not y in ( still_not-bound_in h) implies (( Ex (x,p)) => ( Ex (x,y,q))) is valid

    proof

      assume p = (h . x) & q = (h . y) & not y in ( still_not-bound_in h);

      then ( All (x,(p => ( Ex (y,q))))) is valid by Th22, Th23;

      then (( Ex (x,p)) => ( Ex (x,( Ex (y,q))))) is valid by Th35;

      hence thesis by QC_LANG2: 14;

    end;

    theorem :: CQC_THE2:59

    (( Ex (x,( All (y,p)))) => ( All (y,( Ex (x,p))))) is valid

    proof

       not x in ( still_not-bound_in ( Ex (x,p))) by Th6;

      then

       A1: not x in ( still_not-bound_in ( All (y,( Ex (x,p))))) by Th5;

      ( All (y,(p => ( Ex (x,p))))) is valid & (( All (y,(p => ( Ex (x,p))))) => (( All (y,p)) => ( All (y,( Ex (x,p)))))) is valid by Th15, Th23, Th30;

      then (( All (y,p)) => ( All (y,( Ex (x,p))))) is valid by CQC_THE1: 65;

      hence thesis by A1, Th19;

    end;

    theorem :: CQC_THE2:60

    ( Ex (x,(p <=> p))) is valid by Lm13, Th16;

    theorem :: CQC_THE2:61

    

     Th61: (( Ex (x,(p => q))) => (( All (x,p)) => ( Ex (x,q)))) is valid & ((( All (x,p)) => ( Ex (x,q))) => ( Ex (x,(p => q)))) is valid

    proof

      (( All (x,p)) => p) is valid by CQC_THE1: 66;

      then

       A1: ((p => q) => (( All (x,p)) => q)) is valid by LUKASI_1: 41;

      ( not x in ( still_not-bound_in ( All (x,p)))) & not x in ( still_not-bound_in ( Ex (x,q))) by Th5, Th6;

      then

       A2: not x in ( still_not-bound_in (( All (x,p)) => ( Ex (x,q)))) by Th7;

      (q => ( Ex (x,q))) is valid by Th15;

      then ((p => q) => (( All (x,p)) => ( Ex (x,q)))) is valid by A1, Lm16;

      hence (( Ex (x,(p => q))) => (( All (x,p)) => ( Ex (x,q)))) is valid by A2, Th19;

      (( All (x,(p '&' ( 'not' q)))) => (( All (x,p)) '&' ( All (x,( 'not' q))))) is valid by Th36;

      then

       A3: (( 'not' (( All (x,p)) '&' ( All (x,( 'not' q))))) => ( 'not' ( All (x,(p '&' ( 'not' q)))))) is valid by LUKASI_1: 52;

      (( 'not' ( All (x,(p '&' ( 'not' q))))) => ( Ex (x,( 'not' (p '&' ( 'not' q)))))) is valid by Th51;

      then (( 'not' (( All (x,p)) '&' ( All (x,( 'not' q))))) => ( Ex (x,( 'not' (p '&' ( 'not' q)))))) is valid by A3, LUKASI_1: 42;

      then

       A4: (( 'not' (( All (x,p)) '&' ( All (x,( 'not' q))))) => ( Ex (x,(p => q)))) is valid by QC_LANG2:def 2;

      (( All (x,( 'not' q))) => ( 'not' ( 'not' ( All (x,( 'not' q)))))) is valid;

      then

       A5: ((( All (x,p)) '&' ( All (x,( 'not' q)))) => (( All (x,p)) '&' ( 'not' ( 'not' ( All (x,( 'not' q))))))) is valid by Lm9;

      (( All (x,p)) => ( Ex (x,q))) = (( All (x,p)) => ( 'not' ( All (x,( 'not' q))))) by QC_LANG2:def 5

      .= ( 'not' (( All (x,p)) '&' ( 'not' ( 'not' ( All (x,( 'not' q))))))) by QC_LANG2:def 2;

      then ((( All (x,p)) => ( Ex (x,q))) => ( 'not' (( All (x,p)) '&' ( All (x,( 'not' q)))))) is valid by A5, LUKASI_1: 52;

      hence thesis by A4, LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:62

    

     Th62: (( Ex (x,(p => q))) <=> (( All (x,p)) => ( Ex (x,q)))) is valid

    proof

      (( Ex (x,(p => q))) => (( All (x,p)) => ( Ex (x,q)))) is valid & ((( All (x,p)) => ( Ex (x,q))) => ( Ex (x,(p => q)))) is valid by Th61;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:63

    ( Ex (x,(p => q))) is valid iff (( All (x,p)) => ( Ex (x,q))) is valid

    proof

      (( Ex (x,(p => q))) <=> (( All (x,p)) => ( Ex (x,q)))) is valid by Th62;

      hence thesis by Lm15;

    end;

    theorem :: CQC_THE2:64

    

     Th64: (( All (x,(p '&' q))) => (p '&' ( All (x,q)))) is valid

    proof

      

       A1: (( All (x,(p '&' q))) => (p '&' q)) is valid by CQC_THE1: 66;

      

       A2: not x in ( still_not-bound_in ( All (x,(p '&' q)))) by Th5;

      ((p '&' q) => q) is valid by Lm1;

      then (( All (x,(p '&' q))) => q) is valid by A1, LUKASI_1: 42;

      then

       A3: (( All (x,(p '&' q))) => ( All (x,q))) is valid by A2, CQC_THE1: 67;

      ((p '&' q) => p) is valid by Lm1;

      then (( All (x,(p '&' q))) => p) is valid by A1, LUKASI_1: 42;

      hence thesis by A3, Lm3;

    end;

    theorem :: CQC_THE2:65

    

     Th65: (( All (x,(p '&' q))) => (( All (x,p)) '&' q)) is valid

    proof

      

       A1: ((q '&' ( All (x,p))) => (( All (x,p)) '&' q)) is valid by CQC_THE1: 64;

      ( All (x,((p '&' q) => (q '&' p)))) is valid & (( All (x,((p '&' q) => (q '&' p)))) => (( All (x,(p '&' q))) => ( All (x,(q '&' p))))) is valid by Th23, Th30, CQC_THE1: 64;

      then

       A2: (( All (x,(p '&' q))) => ( All (x,(q '&' p)))) is valid by CQC_THE1: 65;

      (( All (x,(q '&' p))) => (q '&' ( All (x,p)))) is valid by Th64;

      then (( All (x,(p '&' q))) => (q '&' ( All (x,p)))) is valid by A2, LUKASI_1: 42;

      hence thesis by A1, LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:66

    

     Th66: not x in ( still_not-bound_in p) implies ((p '&' ( All (x,q))) => ( All (x,(p '&' q)))) is valid

    proof

      assume

       A1: not x in ( still_not-bound_in p);

      (( All (x,q)) => q) is valid by CQC_THE1: 66;

      then

       A2: ((p '&' ( All (x,q))) => (p '&' q)) is valid by Lm9;

       not x in ( still_not-bound_in ( All (x,q))) by Th5;

      then not x in ( still_not-bound_in (p '&' ( All (x,q)))) by A1, Th8;

      hence thesis by A2, CQC_THE1: 67;

    end;

    theorem :: CQC_THE2:67

     not x in ( still_not-bound_in p) & (p '&' ( All (x,q))) is valid implies ( All (x,(p '&' q))) is valid

    proof

      assume that

       A1: not x in ( still_not-bound_in p) and

       A2: (p '&' ( All (x,q))) is valid;

      ((p '&' ( All (x,q))) => ( All (x,(p '&' q)))) is valid by A1, Th66;

      hence thesis by A2, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:68

    

     Th68: not x in ( still_not-bound_in p) implies ((p 'or' ( All (x,q))) => ( All (x,(p 'or' q)))) is valid & (( All (x,(p 'or' q))) => (p 'or' ( All (x,q)))) is valid

    proof

      

       A1: not x in ( still_not-bound_in ( All (x,(p 'or' q)))) by Th5;

      (( All (x,(p 'or' q))) => (p 'or' q)) is valid & ((p 'or' q) => (( 'not' p) => q)) is valid by Lm11, CQC_THE1: 66;

      then (( All (x,(p 'or' q))) => (( 'not' p) => q)) is valid by LUKASI_1: 42;

      then

       A2: ((( All (x,(p 'or' q))) '&' ( 'not' p)) => q) is valid by Th1;

      assume

       A3: not x in ( still_not-bound_in p);

      then not x in ( still_not-bound_in ( 'not' p)) by QC_LANG3: 7;

      then not x in ( still_not-bound_in (( All (x,(p 'or' q))) '&' ( 'not' p))) by A1, Th8;

      then ((( All (x,(p 'or' q))) '&' ( 'not' p)) => ( All (x,q))) is valid by A2, CQC_THE1: 67;

      then

       A4: (( All (x,(p 'or' q))) => (( 'not' p) => ( All (x,q)))) is valid by Th3;

      (p => p) is valid;

      then (p => ( All (x,p))) is valid by A3, CQC_THE1: 67;

      then

       A5: ((p 'or' ( All (x,q))) => (( All (x,p)) 'or' ( All (x,q)))) is valid by Lm10;

      ((( All (x,p)) 'or' ( All (x,q))) => ( All (x,(p 'or' q)))) is valid by Th39;

      hence ((p 'or' ( All (x,q))) => ( All (x,(p 'or' q)))) is valid by A5, LUKASI_1: 42;

      ((( 'not' p) => ( All (x,q))) => (p 'or' ( All (x,q)))) is valid by Lm12;

      hence thesis by A4, LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:69

    

     Th69: not x in ( still_not-bound_in p) implies ((p 'or' ( All (x,q))) <=> ( All (x,(p 'or' q)))) is valid

    proof

      assume not x in ( still_not-bound_in p);

      then ((p 'or' ( All (x,q))) => ( All (x,(p 'or' q)))) is valid & (( All (x,(p 'or' q))) => (p 'or' ( All (x,q)))) is valid by Th68;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:70

     not x in ( still_not-bound_in p) implies ((p 'or' ( All (x,q))) is valid iff ( All (x,(p 'or' q))) is valid)

    proof

      assume not x in ( still_not-bound_in p);

      then ((p 'or' ( All (x,q))) <=> ( All (x,(p 'or' q)))) is valid by Th69;

      hence thesis by Lm15;

    end;

    theorem :: CQC_THE2:71

    

     Th71: not x in ( still_not-bound_in p) implies ((p '&' ( Ex (x,q))) => ( Ex (x,(p '&' q)))) is valid & (( Ex (x,(p '&' q))) => (p '&' ( Ex (x,q)))) is valid

    proof

      assume

       A1: not x in ( still_not-bound_in p);

      ((p '&' q) => ( Ex (x,(p '&' q)))) is valid by Th15;

      then

       A2: (q => (p => ( Ex (x,(p '&' q))))) is valid by Th4;

       not x in ( still_not-bound_in ( Ex (x,(p '&' q)))) by Th6;

      then not x in ( still_not-bound_in (p => ( Ex (x,(p '&' q))))) by A1, Th7;

      then (( Ex (x,q)) => (p => ( Ex (x,(p '&' q))))) is valid by A2, Th19;

      hence ((p '&' ( Ex (x,q))) => ( Ex (x,(p '&' q)))) is valid by Th2;

      (q => ( Ex (x,q))) is valid by Th15;

      then

       A3: ((p '&' q) => (p '&' ( Ex (x,q)))) is valid by Lm9;

       not x in ( still_not-bound_in ( Ex (x,q))) by Th6;

      then not x in ( still_not-bound_in (p '&' ( Ex (x,q)))) by A1, Th8;

      hence thesis by A3, Th19;

    end;

    theorem :: CQC_THE2:72

    

     Th72: not x in ( still_not-bound_in p) implies ((p '&' ( Ex (x,q))) <=> ( Ex (x,(p '&' q)))) is valid

    proof

      assume not x in ( still_not-bound_in p);

      then ((p '&' ( Ex (x,q))) => ( Ex (x,(p '&' q)))) is valid & (( Ex (x,(p '&' q))) => (p '&' ( Ex (x,q)))) is valid by Th71;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:73

     not x in ( still_not-bound_in p) implies ((p '&' ( Ex (x,q))) is valid iff ( Ex (x,(p '&' q))) is valid)

    proof

      assume not x in ( still_not-bound_in p);

      then ((p '&' ( Ex (x,q))) <=> ( Ex (x,(p '&' q)))) is valid by Th72;

      hence thesis by Lm15;

    end;

    

     Lm17: not x in ( still_not-bound_in p) implies (( All (x,(p => q))) => (p => ( All (x,q)))) is valid

    proof

      assume not x in ( still_not-bound_in p);

      then

       A1: (p => ( All (x,p))) is valid by Th24;

      (( All (x,(p => q))) => (( All (x,p)) => ( All (x,q)))) is valid by Th30;

      then (( All (x,p)) => (( All (x,(p => q))) => ( All (x,q)))) is valid by LUKASI_1: 44;

      then (p => (( All (x,(p => q))) => ( All (x,q)))) is valid by A1, LUKASI_1: 42;

      hence thesis by LUKASI_1: 44;

    end;

    theorem :: CQC_THE2:74

    

     Th74: not x in ( still_not-bound_in p) implies (( All (x,(p => q))) => (p => ( All (x,q)))) is valid & ((p => ( All (x,q))) => ( All (x,(p => q)))) is valid

    proof

      assume

       A1: not x in ( still_not-bound_in p);

      hence (( All (x,(p => q))) => (p => ( All (x,q)))) is valid by Lm17;

       not x in ( still_not-bound_in ( All (x,q))) by Th5;

      then not x in ( still_not-bound_in (p => ( All (x,q)))) by A1, Th7;

      then

       A2: (( All (x,((p => ( All (x,q))) => (p => q)))) => ((p => ( All (x,q))) => ( All (x,(p => q))))) is valid by Lm17;

      ( All (x,((( All (x,q)) => q) => ((p => ( All (x,q))) => (p => q))))) is valid & (( All (x,((( All (x,q)) => q) => ((p => ( All (x,q))) => (p => q))))) => (( All (x,(( All (x,q)) => q))) => ( All (x,((p => ( All (x,q))) => (p => q)))))) is valid by Th23, Th30;

      then

       A3: (( All (x,(( All (x,q)) => q))) => ( All (x,((p => ( All (x,q))) => (p => q))))) is valid by CQC_THE1: 65;

      ( All (x,(( All (x,q)) => q))) is valid by Th23, CQC_THE1: 66;

      then ( All (x,((p => ( All (x,q))) => (p => q)))) is valid by A3, CQC_THE1: 65;

      hence thesis by A2, CQC_THE1: 65;

    end;

    theorem :: CQC_THE2:75

    

     Th75: not x in ( still_not-bound_in p) implies ((p => ( All (x,q))) <=> ( All (x,(p => q)))) is valid

    proof

      assume not x in ( still_not-bound_in p);

      then ((p => ( All (x,q))) => ( All (x,(p => q)))) is valid & (( All (x,(p => q))) => (p => ( All (x,q)))) is valid by Th74;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:76

     not x in ( still_not-bound_in p) implies (( All (x,(p => q))) is valid iff (p => ( All (x,q))) is valid)

    proof

      assume not x in ( still_not-bound_in p);

      then ((p => ( All (x,q))) <=> ( All (x,(p => q)))) is valid by Th75;

      hence thesis by Lm15;

    end;

    theorem :: CQC_THE2:77

    

     Th77: not x in ( still_not-bound_in q) implies (( Ex (x,(p => q))) => (( All (x,p)) => q)) is valid

    proof

      assume

       A1: not x in ( still_not-bound_in q);

       not x in ( still_not-bound_in ( All (x,p))) by Th5;

      then not x in ( still_not-bound_in (( All (x,p)) => q)) by A1, Th7;

      then

       A2: (( Ex (x,(( All (x,p)) => q))) => (( All (x,p)) => q)) is valid by Th20;

      (( All (x,p)) => p) is valid by CQC_THE1: 66;

      then

       A3: ( All (x,((p => q) => (( All (x,p)) => q)))) is valid by Th23, LUKASI_1: 41;

      (( All (x,((p => q) => (( All (x,p)) => q)))) => (( Ex (x,(p => q))) => ( Ex (x,(( All (x,p)) => q))))) is valid by Th34;

      then (( Ex (x,(p => q))) => ( Ex (x,(( All (x,p)) => q)))) is valid by A3, CQC_THE1: 65;

      hence thesis by A2, LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:78

    

     Th78: ((( All (x,p)) => q) => ( Ex (x,(p => q)))) is valid

    proof

      (( All (x,(p '&' ( 'not' q)))) => (( All (x,p)) '&' ( 'not' q))) is valid by Th65;

      then (( 'not' (( All (x,p)) '&' ( 'not' q))) => ( 'not' ( All (x,(p '&' ( 'not' q)))))) is valid by LUKASI_1: 52;

      then

       A1: ((( All (x,p)) => q) => ( 'not' ( All (x,(p '&' ( 'not' q)))))) is valid by QC_LANG2:def 2;

      ( All (x,(( 'not' ( 'not' (p '&' ( 'not' q)))) => (p '&' ( 'not' q))))) is valid & (( All (x,(( 'not' ( 'not' (p '&' ( 'not' q)))) => (p '&' ( 'not' q))))) => (( All (x,( 'not' ( 'not' (p '&' ( 'not' q)))))) => ( All (x,(p '&' ( 'not' q)))))) is valid by Th23, Th30;

      then (( All (x,( 'not' ( 'not' (p '&' ( 'not' q)))))) => ( All (x,(p '&' ( 'not' q))))) is valid by CQC_THE1: 65;

      then (( 'not' ( All (x,(p '&' ( 'not' q))))) => ( 'not' ( All (x,( 'not' ( 'not' (p '&' ( 'not' q)))))))) is valid by LUKASI_1: 52;

      then ((( All (x,p)) => q) => ( 'not' ( All (x,( 'not' ( 'not' (p '&' ( 'not' q)))))))) is valid by A1, LUKASI_1: 42;

      then ((( All (x,p)) => q) => ( Ex (x,( 'not' (p '&' ( 'not' q)))))) is valid by QC_LANG2:def 5;

      hence thesis by QC_LANG2:def 2;

    end;

    theorem :: CQC_THE2:79

     not x in ( still_not-bound_in q) implies ((( All (x,p)) => q) is valid iff ( Ex (x,(p => q))) is valid)

    proof

      assume not x in ( still_not-bound_in q);

      then

       A1: (( Ex (x,(p => q))) => (( All (x,p)) => q)) is valid by Th77;

      ((( All (x,p)) => q) => ( Ex (x,(p => q)))) is valid by Th78;

      then ((( All (x,p)) => q) <=> ( Ex (x,(p => q)))) is valid by A1, Lm14;

      hence thesis by Lm15;

    end;

    theorem :: CQC_THE2:80

    

     Th80: not x in ( still_not-bound_in q) implies ((( Ex (x,p)) => q) => ( All (x,(p => q)))) is valid & (( All (x,(p => q))) => (( Ex (x,p)) => q)) is valid

    proof

      assume

       A1: not x in ( still_not-bound_in q);

      (p => ( Ex (x,p))) is valid by Th15;

      then

       A2: ((( Ex (x,p)) => q) => (p => q)) is valid by LUKASI_1: 41;

       not x in ( still_not-bound_in ( Ex (x,p))) by Th6;

      then not x in ( still_not-bound_in (( Ex (x,p)) => q)) by A1, Th7;

      hence ((( Ex (x,p)) => q) => ( All (x,(p => q)))) is valid by A2, CQC_THE1: 67;

      (( All (x,(p => q))) => (( Ex (x,p)) => ( Ex (x,q)))) is valid by Th34;

      then

       A3: ((( All (x,(p => q))) '&' ( Ex (x,p))) => ( Ex (x,q))) is valid by Th1;

      (( Ex (x,q)) => q) is valid by A1, Th20;

      then ((( All (x,(p => q))) '&' ( Ex (x,p))) => q) is valid by A3, LUKASI_1: 42;

      hence thesis by Th3;

    end;

    theorem :: CQC_THE2:81

    

     Th81: not x in ( still_not-bound_in q) implies ((( Ex (x,p)) => q) <=> ( All (x,(p => q)))) is valid

    proof

      assume not x in ( still_not-bound_in q);

      then ((( Ex (x,p)) => q) => ( All (x,(p => q)))) is valid & (( All (x,(p => q))) => (( Ex (x,p)) => q)) is valid by Th80;

      hence thesis by Lm14;

    end;

    theorem :: CQC_THE2:82

     not x in ( still_not-bound_in q) implies ((( Ex (x,p)) => q) is valid iff ( All (x,(p => q))) is valid)

    proof

      assume not x in ( still_not-bound_in q);

      then ((( Ex (x,p)) => q) <=> ( All (x,(p => q)))) is valid by Th81;

      hence thesis by Lm15;

    end;

    theorem :: CQC_THE2:83

    

     Th83: not x in ( still_not-bound_in p) implies (( Ex (x,(p => q))) => (p => ( Ex (x,q)))) is valid

    proof

      assume

       A1: not x in ( still_not-bound_in p);

       not x in ( still_not-bound_in ( Ex (x,q))) by Th6;

      then not x in ( still_not-bound_in (p => ( Ex (x,q)))) by A1, Th7;

      then

       A2: (( Ex (x,(p => ( Ex (x,q))))) => (p => ( Ex (x,q)))) is valid by Th20;

      (q => ( Ex (x,q))) is valid by Th15;

      then

       A3: ( All (x,((p => q) => (p => ( Ex (x,q)))))) is valid by Th23, LUKASI_1: 51;

      (( All (x,((p => q) => (p => ( Ex (x,q)))))) => (( Ex (x,(p => q))) => ( Ex (x,(p => ( Ex (x,q))))))) is valid by Th34;

      then (( Ex (x,(p => q))) => ( Ex (x,(p => ( Ex (x,q)))))) is valid by A3, CQC_THE1: 65;

      hence thesis by A2, LUKASI_1: 42;

    end;

    theorem :: CQC_THE2:84

    

     Th84: ((p => ( Ex (x,q))) => ( Ex (x,(p => q)))) is valid

    proof

      ( All (x,(( 'not' ( 'not' (p '&' ( 'not' q)))) => (p '&' ( 'not' q))))) is valid & (( All (x,(( 'not' ( 'not' (p '&' ( 'not' q)))) => (p '&' ( 'not' q))))) => (( All (x,( 'not' ( 'not' (p '&' ( 'not' q)))))) => ( All (x,(p '&' ( 'not' q)))))) is valid by Th23, Th30;

      then (( All (x,( 'not' ( 'not' (p '&' ( 'not' q)))))) => ( All (x,(p '&' ( 'not' q))))) is valid by CQC_THE1: 65;

      then

       A1: (( 'not' ( All (x,(p '&' ( 'not' q))))) => ( 'not' ( All (x,( 'not' ( 'not' (p '&' ( 'not' q)))))))) is valid by LUKASI_1: 52;

      (( All (x,( 'not' q))) <=> ( 'not' ( Ex (x,q)))) is valid by Th54;

      then (( All (x,( 'not' q))) => ( 'not' ( Ex (x,q)))) is valid by Lm14;

      then ((p '&' ( All (x,( 'not' q)))) => (p '&' ( 'not' ( Ex (x,q))))) is valid by Lm9;

      then

       A2: (( 'not' (p '&' ( 'not' ( Ex (x,q))))) => ( 'not' (p '&' ( All (x,( 'not' q)))))) is valid by LUKASI_1: 52;

      (( All (x,(p '&' ( 'not' q)))) => (p '&' ( All (x,( 'not' q))))) is valid by Th64;

      then (( 'not' (p '&' ( All (x,( 'not' q))))) => ( 'not' ( All (x,(p '&' ( 'not' q)))))) is valid by LUKASI_1: 52;

      then (( 'not' (p '&' ( 'not' ( Ex (x,q))))) => ( 'not' ( All (x,(p '&' ( 'not' q)))))) is valid by A2, LUKASI_1: 42;

      then ((p => ( Ex (x,q))) => ( 'not' ( All (x,(p '&' ( 'not' q)))))) is valid by QC_LANG2:def 2;

      then ((p => ( Ex (x,q))) => ( 'not' ( All (x,( 'not' ( 'not' (p '&' ( 'not' q)))))))) is valid by A1, LUKASI_1: 42;

      then ((p => ( Ex (x,q))) => ( 'not' ( All (x,( 'not' (p => q)))))) is valid by QC_LANG2:def 2;

      hence thesis by QC_LANG2:def 5;

    end;

    theorem :: CQC_THE2:85

    

     Th85: not x in ( still_not-bound_in p) implies ((p => ( Ex (x,q))) <=> ( Ex (x,(p => q)))) is valid

    proof

      assume not x in ( still_not-bound_in p);

      then

       A1: (( Ex (x,(p => q))) => (p => ( Ex (x,q)))) is valid by Th83;

      ((p => ( Ex (x,q))) => ( Ex (x,(p => q)))) is valid by Th84;

      hence thesis by A1, Lm14;

    end;

    theorem :: CQC_THE2:86

     not x in ( still_not-bound_in p) implies ((p => ( Ex (x,q))) is valid iff ( Ex (x,(p => q))) is valid)

    proof

      assume not x in ( still_not-bound_in p);

      then ((p => ( Ex (x,q))) <=> ( Ex (x,(p => q)))) is valid by Th85;

      hence thesis by Lm15;

    end;

    theorem :: CQC_THE2:87

     {p} |- p

    proof

      p in {p} & {p} c= ( Cn {p}) by CQC_THE1: 17, TARSKI:def 1;

      hence p in ( Cn {p});

    end;

    theorem :: CQC_THE2:88

    

     Th88: ( Cn ( {p} \/ {q})) = ( Cn {(p '&' q)})

    proof

      for t holds t in ( Cn ( {p} \/ {q})) iff for T st T is being_a_theory & {(p '&' q)} c= T holds t in T

      proof

        let t;

        thus t in ( Cn ( {p} \/ {q})) implies for T st T is being_a_theory & {(p '&' q)} c= T holds t in T

        proof

          assume

           A1: t in ( Cn ( {p} \/ {q}));

          let T;

          assume that

           A2: T is being_a_theory and

           A3: {(p '&' q)} c= T;

          

           A4: (p '&' q) in T & ( TAUT A) c= T by A2, A3, CQC_THE1: 38, ZFMISC_1: 31;

          ((p '&' q) => q) in ( TAUT A) by PROCAL_1: 21;

          then q in T by A2, A4;

          then

           A5: {q} c= T by ZFMISC_1: 31;

          ((p '&' q) => p) in ( TAUT A) by PROCAL_1: 19;

          then p in T by A2, A4;

          then {p} c= T by ZFMISC_1: 31;

          then ( {p} \/ {q}) c= T by A5, XBOOLE_1: 8;

          hence thesis by A1, A2, CQC_THE1:def 2;

        end;

        thus (for T st T is being_a_theory & {(p '&' q)} c= T holds t in T) implies t in ( Cn ( {p} \/ {q}))

        proof

          assume

           A6: for T st T is being_a_theory & {(p '&' q)} c= T holds t in T;

          for T st T is being_a_theory & ( {p} \/ {q}) c= T holds t in T

          proof

            let T;

            assume that

             A7: T is being_a_theory and

             A8: ( {p} \/ {q}) c= T;

             {p} c= ( {p} \/ {q}) by XBOOLE_1: 7;

            then {p} c= T by A8, XBOOLE_1: 1;

            then

             A9: p in T by ZFMISC_1: 31;

             {q} c= ( {p} \/ {q}) by XBOOLE_1: 7;

            then {q} c= T by A8, XBOOLE_1: 1;

            then

             A10: q in T by ZFMISC_1: 31;

            (p => (q => (p '&' q))) in ( TAUT A) & ( TAUT A) c= T by A7, CQC_THE1: 38, PROCAL_1: 28;

            then (q => (p '&' q)) in T by A7, A9;

            then (p '&' q) in T by A7, A10;

            then {(p '&' q)} c= T by ZFMISC_1: 31;

            hence thesis by A6, A7;

          end;

          hence thesis by CQC_THE1:def 2;

        end;

      end;

      hence thesis by CQC_THE1:def 2;

    end;

    theorem :: CQC_THE2:89

     {p, q} |- r iff {(p '&' q)} |- r

    proof

      thus {p, q} |- r implies {(p '&' q)} |- r

      proof

        assume r in ( Cn {p, q});

        then r in ( Cn ( {p} \/ {q})) by ENUMSET1: 1;

        hence r in ( Cn {(p '&' q)}) by Th88;

      end;

      assume r in ( Cn {(p '&' q)});

      then r in ( Cn ( {p} \/ {q})) by Th88;

      hence r in ( Cn {p, q}) by ENUMSET1: 1;

    end;

    theorem :: CQC_THE2:90

    

     Th90: X |- p implies X |- ( All (x,p))

    proof

      

       A1: X |- (p => ((( All (x,p)) => ( All (x,p))) => p)) by CQC_THE1: 59;

       not x in ( still_not-bound_in ( All (x,p))) by Th5;

      then

       A2: not x in ( still_not-bound_in (( All (x,p)) => ( All (x,p)))) by Th7;

      assume X |- p;

      then X |- ((( All (x,p)) => ( All (x,p))) => p) by A1, CQC_THE1: 55;

      then

       A3: X |- ((( All (x,p)) => ( All (x,p))) => ( All (x,p))) by A2, CQC_THE1: 57;

      X |- (( All (x,p)) => ( All (x,p))) by CQC_THE1: 59;

      hence thesis by A3, CQC_THE1: 55;

    end;

    theorem :: CQC_THE2:91

     not x in ( still_not-bound_in p) implies X |- (( All (x,(p => q))) => (p => ( All (x,q)))) by Th74, CQC_THE1: 59;

    ::$Notion-Name

    theorem :: CQC_THE2:92

    F is closed & (X \/ {F}) |- G implies X |- (F => G)

    proof

      assume that

       A1: F is closed and

       A2: (X \/ {F}) |- G;

      G in ( Cn (X \/ {F})) by A2;

      then

      consider f such that

       A3: f is_a_proof_wrt (X \/ {F}) and

       A4: ( Effect f) = G by CQC_THE1: 36;

      f <> {} by A3;

      then

       A5: G = ((f . ( len f)) `1 ) by A4, CQC_THE1:def 6;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies for H st H = ((f . $1) `1 ) holds X |- (F => H);

      

       A6: for n be Nat st for k be Nat st k < n holds P[k] holds P[n]

      proof

        let n be Nat such that

         A7: for k be Nat st k < n holds 1 <= k & k <= ( len f) implies for H st H = ((f . k) `1 ) holds X |- (F => H);

        assume that

         A8: 1 <= n and

         A9: n <= ( len f);

        

         A10: (f,n) is_a_correct_step_wrt (X \/ {F}) by A3, A8, A9;

        let H such that

         A11: H = ((f . n) `1 );

        now

          ((f . n) `2 ) = 0 or ... or ((f . n) `2 ) = 9 by A8, A9, CQC_THE1: 23;

          per cases ;

            suppose ((f . n) `2 ) = 0 ;

            then H in (X \/ {F}) by A11, A10, CQC_THE1:def 4;

            then

             A12: H in X or H in {F} by XBOOLE_0:def 3;

            now

              per cases by A12, TARSKI:def 1;

                suppose

                 A13: H in X;

                X c= ( Cn X) by CQC_THE1: 17;

                then

                 A14: X |- H by A13;

                X |- (H => (F => H)) by CQC_THE1: 59;

                hence thesis by A14, CQC_THE1: 55;

              end;

                suppose H = F;

                hence thesis by CQC_THE1: 59;

              end;

            end;

            hence thesis;

          end;

            suppose ((f . n) `2 ) = 1;

            then H = ( VERUM A) by A11, A10, CQC_THE1:def 4;

            hence thesis by CQC_THE1: 59, LUKASI_1: 46;

          end;

            suppose ((f . n) `2 ) = 2;

            then ex p st H = ((( 'not' p) => p) => p) by A11, A10, CQC_THE1:def 4;

            then H is valid by CQC_THE1: 61;

            hence thesis by CQC_THE1: 59, LUKASI_1: 61;

          end;

            suppose ((f . n) `2 ) = 3;

            then ex p, q st H = (p => (( 'not' p) => q)) by A11, A10, CQC_THE1:def 4;

            then H is valid by CQC_THE1: 62;

            hence thesis by CQC_THE1: 59, LUKASI_1: 61;

          end;

            suppose ((f . n) `2 ) = 4;

            then ex p, q, r st H = ((p => q) => (( 'not' (q '&' r)) => ( 'not' (p '&' r)))) by A11, A10, CQC_THE1:def 4;

            then H is valid by CQC_THE1: 63;

            hence thesis by CQC_THE1: 59, LUKASI_1: 61;

          end;

            suppose ((f . n) `2 ) = 5;

            then ex p, q st H = ((p '&' q) => (q '&' p)) by A11, A10, CQC_THE1:def 4;

            then H is valid by CQC_THE1: 64;

            hence thesis by CQC_THE1: 59, LUKASI_1: 61;

          end;

            suppose ((f . n) `2 ) = 6;

            then ex p, x st H = (( All (x,p)) => p) by A11, A10, CQC_THE1:def 4;

            then H is valid by CQC_THE1: 66;

            hence thesis by CQC_THE1: 59, LUKASI_1: 61;

          end;

            suppose ((f . n) `2 ) = 7;

            then

            consider i,j be Nat, p, q such that

             A15: 1 <= i and

             A16: i < n and

             A17: 1 <= j and

             A18: j < i and

             A19: p = ((f . j) `1 ) and

             A20: q = H and

             A21: ((f . i) `1 ) = (p => q) by A11, A10, CQC_THE1:def 4;

            i <= ( len f) by A9, A16, XXREAL_0: 2;

            then

             A22: X |- (F => (p => q)) by A7, A15, A16, A21;

            X |- ((F => (p => q)) => ((F => p) => (F => q))) by CQC_THE1: 59;

            then

             A23: X |- ((F => p) => (F => q)) by A22, CQC_THE1: 55;

            j < n by A16, A18, XXREAL_0: 2;

            then

             A24: j <= ( len f) by A9, XXREAL_0: 2;

            j < n by A16, A18, XXREAL_0: 2;

            then X |- (F => p) by A7, A17, A19, A24;

            hence thesis by A20, A23, CQC_THE1: 55;

          end;

            suppose ((f . n) `2 ) = 8;

            then

            consider i be Nat, p, q, x such that

             A25: 1 <= i and

             A26: i < n and

             A27: ((f . i) `1 ) = (p => q) and

             A28: not x in ( still_not-bound_in p) and

             A29: H = (p => ( All (x,q))) by A11, A10, CQC_THE1:def 4;

            

             A30: X |- (( All (x,(p => q))) => (p => ( All (x,q)))) by A28, Th74, CQC_THE1: 59;

             not x in ( still_not-bound_in F) by A1, QC_LANG1:def 31;

            then

             A31: X |- (( All (x,(F => (p => q)))) => (F => ( All (x,(p => q))))) by Th74, CQC_THE1: 59;

            i <= ( len f) by A9, A26, XXREAL_0: 2;

            then X |- ( All (x,(F => (p => q)))) by A7, A25, A26, A27, Th90;

            then X |- (F => ( All (x,(p => q)))) by A31, CQC_THE1: 55;

            hence thesis by A29, A30, LUKASI_1: 59;

          end;

            suppose ((f . n) `2 ) = 9;

            then

            consider i be Nat, x, y, s such that

             A32: 1 <= i and

             A33: i < n and

             A34: (s . x) in ( CQC-WFF A) & (s . y) in ( CQC-WFF A) and

             A35: not x in ( still_not-bound_in s) and

             A36: (s . x) = ((f . i) `1 ) and

             A37: H = (s . y) by A11, A10, CQC_THE1:def 4;

            reconsider s1 = (s . x), s2 = (s . y) as Element of ( CQC-WFF A) by A34;

            

             A38: X |- (( All (x,s1)) => s2) by A35, Th25, CQC_THE1: 59;

             not x in ( still_not-bound_in F) by A1, QC_LANG1:def 31;

            then

             A39: X |- (( All (x,(F => s1))) => (F => ( All (x,s1)))) by Th74, CQC_THE1: 59;

            i <= ( len f) by A9, A33, XXREAL_0: 2;

            then X |- ( All (x,(F => s1))) by A7, A32, A33, A36, Th90;

            then X |- (F => ( All (x,s1))) by A39, CQC_THE1: 55;

            hence thesis by A37, A38, LUKASI_1: 59;

          end;

        end;

        hence thesis;

      end;

      

       A40: for n be Nat holds P[n] from NAT_1:sch 4( A6);

      1 <= ( len f) by A3, CQC_THE1: 25;

      hence thesis by A40, A5;

    end;