cqc_the3.miz

    begin

    reserve A for QC-alphabet;

    reserve p,q,r,s,p1,q1 for Element of ( CQC-WFF A),

X,Y,Z,X1,X2 for Subset of ( CQC-WFF A),

h for QC-formula of A,

x,y for bound_QC-variable of A,

n for Element of NAT ;

    theorem :: CQC_THE3:1



     Th1: p in X implies X |- p

    proof

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

      hence thesis by CQC_THE1:def 8;

    end;

    theorem :: CQC_THE3:2



     Th2: X c= ( Cn Y) implies ( Cn X) c= ( Cn Y) by CQC_THE1: 15, CQC_THE1: 16;

    theorem :: CQC_THE3:3



     Th3: X |- p & {p} |- q implies X |- q

    proof

      assume that

       A1: X |- p and

       A2: {p} |- q;

      p in ( Cn X) by A1, CQC_THE1:def 8;

      then {p} c= ( Cn X) by ZFMISC_1: 31;

      then

       A3: ( Cn {p}) c= ( Cn X) by CQC_THE1: 15, CQC_THE1: 16;

      q in ( Cn {p}) by A2, CQC_THE1:def 8;

      hence thesis by A3, CQC_THE1:def 8;

    end;

    theorem :: CQC_THE3:4



     Th4: X |- p & X c= Y implies Y |- p

    proof

      assume that

       A1: X |- p and

       A2: X c= Y;



       A3: p in ( Cn X) by A1, CQC_THE1:def 8;

      ( Cn X) c= ( Cn Y) by A2, CQC_THE1: 18;

      hence thesis by A3, CQC_THE1:def 8;

    end;

    definition

      let A;

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

      :: CQC_THE3:def1

      pred p |- q means {p} |- q;

    end

    theorem :: CQC_THE3:5



     Th5: p |- p by CQC_THE2: 87;

    theorem :: CQC_THE3:6



     Th6: p |- q & q |- r implies p |- r by Th3;

    definition

      let A;

      let X,Y be Subset of ( CQC-WFF A);

      :: CQC_THE3:def2

      pred X |- Y means for p be Element of ( CQC-WFF A) st p in Y holds X |- p;

    end

    theorem :: CQC_THE3:7



     Th7: X |- Y iff Y c= ( Cn X)

    proof

      hereby

        assume

         A1: X |- Y;

        now

          let p be object;

          assume

           A2: p in Y;

          then

          reconsider p9 = p as Element of ( CQC-WFF A);

          X |- p9 by A1, A2;

          hence p in ( Cn X) by CQC_THE1:def 8;

        end;

        hence Y c= ( Cn X);

      end;

      thus thesis by CQC_THE1:def 8;

    end;

    theorem :: CQC_THE3:8

    X |- X by Th1;

    theorem :: CQC_THE3:9



     Th9: X |- Y & Y |- Z implies X |- Z

    proof

      assume that

       A1: X |- Y and

       A2: Y |- Z;

      for p st p in Z holds X |- p

      proof

        let p;

        assume p in Z;

        then Y |- p by A2;

        then

         A3: p in ( Cn Y) by CQC_THE1:def 8;

        Y c= ( Cn X) by A1, Th7;

        then ( Cn Y) c= ( Cn X) by CQC_THE1: 15, CQC_THE1: 16;

        hence thesis by A3, CQC_THE1:def 8;

      end;

      hence thesis;

    end;

    theorem :: CQC_THE3:10



     Th10: X |- {p} iff X |- p

    proof

      hereby

        p in {p} by TARSKI:def 1;

        hence X |- {p} implies X |- p;

      end;

      thus thesis by TARSKI:def 1;

    end;

    theorem :: CQC_THE3:11



     Th11: {p} |- {q} iff p |- q by Th10;

    theorem :: CQC_THE3:12

    X c= Y implies Y |- X by Th1;

    theorem :: CQC_THE3:13



     Th13: X |- ( TAUT A)

    proof

      ( TAUT A) c= ( Cn X) by CQC_THE1: 39;

      hence thesis by Th7;

    end;

    theorem :: CQC_THE3:14

    ( {} ( CQC-WFF A)) |- ( TAUT A) by Th13;

    definition

      let A;

      let X be Subset of ( CQC-WFF A);

      :: CQC_THE3:def3

      pred |- X means for p be Element of ( CQC-WFF A) st p in X holds p is valid;

    end

    theorem :: CQC_THE3:15



     Th15: |- X iff ( {} ( CQC-WFF A)) |- X

    proof

      hereby

        assume

         A1: |- X;

        now

          let p;

          assume p in X;

          then p is valid by A1;

          hence ( {} ( CQC-WFF A)) |- p by CQC_THE1:def 9;

        end;

        hence ( {} ( CQC-WFF A)) |- X;

      end;

      thus thesis by CQC_THE1:def 9;

    end;

    theorem :: CQC_THE3:16

     |- ( TAUT A)

    proof



       A1: |- ( TAUT A) iff ( {} ( CQC-WFF A)) |- ( TAUT A) by Th15;

      ( {} ( CQC-WFF A)) |- ( TAUT A) by Th13;

      hence thesis by A1;

    end;

    theorem :: CQC_THE3:17

     |- X iff X c= ( TAUT A)

    proof

      hereby

        assume

         A1: |- X;

        now

          let p;

          assume p in X;

          then p is valid by A1;

          hence p in ( TAUT A) by CQC_THE1:def 10;

        end;

        hence X c= ( TAUT A);

      end;

      thus thesis by CQC_THE1:def 10;

    end;

    definition

      let A, X, Y;

      :: CQC_THE3:def4

      pred X |-| Y means for p holds (X |- p iff Y |- p);

      reflexivity ;

      symmetry ;

    end

    theorem :: CQC_THE3:18



     Th18: X |-| Y iff X |- Y & Y |- X

    proof

      thus X |-| Y implies X |- Y & Y |- X by Th1;

      assume that

       A1: X |- Y and

       A2: Y |- X;

      let p;

       A3:

      now

        assume Y |- p;

        then Y |- {p} by Th10;

        then X |- {p} by A1, Th9;

        hence X |- p by Th10;

      end;

      now

        assume X |- p;

        then X |- {p} by Th10;

        then Y |- {p} by A2, Th9;

        hence Y |- p by Th10;

      end;

      hence X |- p iff Y |- p by A3;

    end;

    theorem :: CQC_THE3:19

    X |-| Y & Y |-| Z implies X |-| Z;

    theorem :: CQC_THE3:20



     Th20: X |-| Y iff ( Cn X) = ( Cn Y)

    proof

       A1:

      now

        assume

         A2: X |-| Y;

        then Y |- X by Th18;

        then X c= ( Cn Y) by Th7;

        then

         A3: ( Cn X) c= ( Cn Y) by CQC_THE1: 15, CQC_THE1: 16;

        X |- Y by A2, Th18;

        then Y c= ( Cn X) by Th7;

        then ( Cn Y) c= ( Cn X) by CQC_THE1: 15, CQC_THE1: 16;

        hence ( Cn X) = ( Cn Y) by A3, XBOOLE_0:def 10;

      end;

      now

        assume

         A4: ( Cn X) = ( Cn Y);

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

        then

         A5: Y |- X by A4, Th7;

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

        then X |- Y by A4, Th7;

        hence X |-| Y by A5, Th18;

      end;

      hence thesis by A1;

    end;



     Lm1: (X \/ Y) c= (( Cn X) \/ ( Cn Y))

    proof



       A1: Y c= ( Cn Y) by CQC_THE1: 17;

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

      hence thesis by A1, XBOOLE_1: 13;

    end;

    theorem :: CQC_THE3:21



     Th21: (( Cn X) \/ ( Cn Y)) c= ( Cn (X \/ Y))

    proof



       A1: ( Cn Y) c= ( Cn (X \/ Y)) by CQC_THE1: 18, XBOOLE_1: 7;

      ( Cn X) c= ( Cn (X \/ Y)) by CQC_THE1: 18, XBOOLE_1: 7;

      hence thesis by A1, XBOOLE_1: 8;

    end;

    theorem :: CQC_THE3:22



     Th22: ( Cn (X \/ Y)) = ( Cn (( Cn X) \/ ( Cn Y)))

    proof



       A1: ( Cn (X \/ Y)) c= ( Cn (( Cn X) \/ ( Cn Y))) by Lm1, CQC_THE1: 18;

      ( Cn (( Cn X) \/ ( Cn Y))) c= ( Cn (X \/ Y)) by Th2, Th21;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: CQC_THE3:23

    X |-| ( Cn X)

    proof

      ( Cn X) = ( Cn ( Cn X)) by CQC_THE1: 19;

      hence thesis by Th20;

    end;

    theorem :: CQC_THE3:24

    (X \/ Y) |-| (( Cn X) \/ ( Cn Y))

    proof

      ( Cn (X \/ Y)) = ( Cn (( Cn X) \/ ( Cn Y))) by Th22;

      hence thesis by Th20;

    end;

    theorem :: CQC_THE3:25



     Th25: X1 |-| X2 implies (X1 \/ Y) |-| (X2 \/ Y)

    proof

      assume X1 |-| X2;

      then ( Cn X1) = ( Cn X2) by Th20;



      then ( Cn (X1 \/ Y)) = ( Cn (( Cn X2) \/ ( Cn Y))) by Th22

      .= ( Cn (X2 \/ Y)) by Th22;

      hence thesis by Th20;

    end;

    theorem :: CQC_THE3:26



     Th26: X1 |-| X2 & (X1 \/ Y) |- Z implies (X2 \/ Y) |- Z

    proof

      assume that

       A1: X1 |-| X2 and

       A2: (X1 \/ Y) |- Z;

      (X1 \/ Y) |-| (X2 \/ Y) by A1, Th25;

      then ( Cn (X1 \/ Y)) = ( Cn (X2 \/ Y)) by Th20;

      then Z c= ( Cn (X2 \/ Y)) by A2, Th7;

      hence thesis by Th7;

    end;

    theorem :: CQC_THE3:27



     Th27: X1 |-| X2 & Y |- X1 implies Y |- X2

    proof

      assume that

       A1: X1 |-| X2 and

       A2: Y |- X1;

      X1 |- X2 by A1, Th18;

      hence thesis by A2, Th9;

    end;

    definition

      let A;

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

      :: CQC_THE3:def5

      pred p |-| q means p |- q & q |- p;

      reflexivity by Th5;

      symmetry ;

    end

    theorem :: CQC_THE3:28



     Th28: p |-| q & q |-| r implies p |-| r by Th6;

    theorem :: CQC_THE3:29



     Th29: p |-| q iff {p} |-| {q}

    proof

       A1:

      now

        assume

         A2: {p} |-| {q};

        then {q} |- {p} by Th18;

        then

         A3: q |- p by Th11;

         {p} |- {q} by A2, Th18;

        then p |- q by Th11;

        hence p |-| q by A3;

      end;

      now

        assume

         A4: p |-| q;

        then q |- p;

        then

         A5: {q} |- {p} by Th11;

        p |- q by A4;

        then {p} |- {q} by Th11;

        hence {p} |-| {q} by A5, Th18;

      end;

      hence thesis by A1;

    end;

    theorem :: CQC_THE3:30

    p |-| q & X |- p implies X |- q

    proof

      assume that

       A1: p |-| q and

       A2: X |- p;



       A3: X |- {p} by A2, Th10;

       {p} |-| {q} by A1, Th29;

      then X |- {q} by A3, Th27;

      hence thesis by Th10;

    end;

    theorem :: CQC_THE3:31



     Th31: {p, q} |-| {(p '&' q)} by CQC_THE2: 89;

    theorem :: CQC_THE3:32

    (p '&' q) |-| (q '&' p)

    proof



       A1: {q, p} |-| {(q '&' p)} by Th31;

       {(p '&' q)} |-| {q, p} by Th31;

      then {(p '&' q)} |-| {(q '&' p)} by A1;

      hence thesis by Th29;

    end;



     Lm2: X |- p & X |- q implies X |- (p '&' q)

    proof

      assume that

       A1: X |- p and

       A2: X |- q;

      for r st r in {p, q} holds X |- r by A1, A2, TARSKI:def 2;

      then X |- {p, q};

      then X |- {(p '&' q)} by Th27, Th31;

      hence thesis by Th10;

    end;



     Lm3: X |- (p '&' q) implies X |- p & X |- q

    proof

      assume X |- (p '&' q);

      then

       A1: X |- {(p '&' q)} by Th10;

       {p, q} |-| {(p '&' q)} by Th31;

      then

       A2: X |- {p, q} by A1, Th27;

      p in {p, q} by TARSKI:def 2;

      hence X |- p by A2;

      q in {p, q} by TARSKI:def 2;

      hence thesis by A2;

    end;

    theorem :: CQC_THE3:33

    X |- (p '&' q) iff X |- p & X |- q by Lm2, Lm3;



     Lm4: p |-| q & r |-| s implies (p '&' r) |- (q '&' s)

    proof

      assume that

       A1: p |-| q and

       A2: r |-| s;

      r |- s by A2;

      then {r} |- s;

      then

       A3: {p, r} |- s by Th4, ZFMISC_1: 7;

       {p, r} |-| {(p '&' r)} by Th31;

      then

       A4: {(p '&' r)} |- {p, r} by Th18;

      p |- q by A1;

      then {p} |- q;

      then {p, r} |- q by Th4, ZFMISC_1: 7;

      then {p, r} |- (q '&' s) by A3, Lm2;

      then {p, r} |- {(q '&' s)} by Th10;

      then {(p '&' r)} |- {(q '&' s)} by A4, Th9;

      hence thesis by Th11;

    end;

    theorem :: CQC_THE3:34

    p |-| q & r |-| s implies (p '&' r) |-| (q '&' s) by Lm4;

    theorem :: CQC_THE3:35



     Th35: X |- ( All (x,p)) iff X |- p

    proof

      thus X |- ( All (x,p)) implies X |- p

      proof



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

        assume X |- ( All (x,p));

        hence thesis by A1, CQC_THE1: 55;

      end;

      thus thesis by CQC_THE2: 90;

    end;

    theorem :: CQC_THE3:36



     Th36: ( All (x,p)) |-| p

    proof

       {( All (x,p))} |- (( All (x,p)) => p) by CQC_THE1: 56;

      then {( All (x,p))} |- p by CQC_THE1: 55, CQC_THE2: 87;

      hence ( All (x,p)) |- p;

       {p} |- p by CQC_THE2: 87;

      then {p} |- ( All (x,p)) by Th35;

      hence thesis;

    end;

    theorem :: CQC_THE3:37

    p |-| q implies ( All (x,p)) |-| ( All (y,q))

    proof

      assume

       A1: p |-| q;



       A2: q |-| ( All (y,q)) by Th36;

      ( All (x,p)) |-| p by Th36;

      then ( All (x,p)) |-| q by A1, Th28;

      hence thesis by A2, Th28;

    end;

    definition

      let A;

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

      :: CQC_THE3:def6

      pred p is_an_universal_closure_of q means p is closed & ex n be Element of NAT st 1 <= n & ex L be FinSequence st ( len L) = n & (L . 1) = q & (L . n) = p & for k be Nat st 1 <= k & k < n holds ex x be bound_QC-variable of A st ex r be Element of ( CQC-WFF A) st r = (L . k) & (L . (k + 1)) = ( All (x,r));

    end

    theorem :: CQC_THE3:38



     Th38: p is_an_universal_closure_of q implies p |-| q

    proof

      assume p is_an_universal_closure_of q;

      then

      consider n be Element of NAT such that

       A1: 1 <= n and

       A2: ex L be FinSequence st ( len L) = n & (L . 1) = q & (L . n) = p & for k be Nat st 1 <= k & k < n holds ex x, r st r = (L . k) & (L . (k + 1)) = ( All (x,r));

      consider L be FinSequence such that ( len L) = n and

       A3: (L . 1) = q and

       A4: (L . n) = p and

       A5: for k be Nat st 1 <= k & k < n holds ex x, r st r = (L . k) & (L . (k + 1)) = ( All (x,r)) by A2;

      for k be Nat st 1 <= k & k <= n holds ex r st r = (L . k) & q |-| r

      proof

        defpred P[ Nat] means 1 <= $1 & $1 <= n implies ex r st r = (L . $1) & q |-| r;



         A6: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A7: P[k];

          now

            assume that 1 <= (k + 1) and

             A8: (k + 1) <= n;

            per cases by A8, NAT_1: 13, NAT_1: 14;

              case

               A9: k = 0 ;

              take p = q;

              thus ex r st r = (L . (k + 1)) & q |-| r by A3, A9;

            end;

              case

               A10: 1 <= k & k < n;

              then

              consider x, r such that

               A11: r = (L . k) and

               A12: (L . (k + 1)) = ( All (x,r)) by A5;

              consider s such that

               A13: s = ( All (x,r));

              s |-| r by A13, Th36;

              hence ex s st s = (L . (k + 1)) & q |-| s by A7, A10, A11, A12, A13, Th28;

            end;

          end;

          hence thesis;

        end;



         A14: P[ 0 ];

        thus for k be Nat holds P[k] from NAT_1:sch 2( A14, A6);

      end;

      then ex r st r = (L . n) & q |-| r by A1;

      hence thesis by A4;

    end;

    theorem :: CQC_THE3:39



     Th39: (p => q) is valid implies p |- q

    proof

      assume (p => q) is valid;

      then {p} |- (p => q) by CQC_THE1: 59;

      then {p} |- q by CQC_THE1: 55, CQC_THE2: 87;

      hence thesis;

    end;

    theorem :: CQC_THE3:40



     Th40: X |- (p => q) implies (X \/ {p}) |- q

    proof

      p in {p} by TARSKI:def 1;

      then p in (X \/ {p}) by XBOOLE_0:def 3;

      then

       A1: (X \/ {p}) |- p by Th1;

      assume X |- (p => q);

      then (X \/ {p}) |- (p => q) by Th4, XBOOLE_1: 7;

      hence thesis by A1, CQC_THE1: 55;

    end;

    theorem :: CQC_THE3:41



     Th41: p is closed & p |- q implies (p => q) is valid

    proof

      assume that

       A1: p is closed and

       A2: p |- q;

      (( {} ( CQC-WFF A)) \/ {p}) |- q by A2;

      then ( {} ( CQC-WFF A)) |- (p => q) by A1, CQC_THE2: 92;

      hence thesis by CQC_THE1:def 9;

    end;

    theorem :: CQC_THE3:42

    p1 is_an_universal_closure_of p implies ((X \/ {p}) |- q iff X |- (p1 => q))

    proof

      assume

       A1: p1 is_an_universal_closure_of p;

      now

        assume (X \/ {p}) |- q;

        then

         A2: (X \/ {p}) |- {q} by Th10;

        p |-| p1 by A1, Th38;

        then {p} |-| {p1} by Th29;

        then (X \/ {p1}) |- {q} by A2, Th26;

        then

         A3: (X \/ {p1}) |- q by Th10;

        p1 is closed by A1;

        hence X |- (p1 => q) by A3, CQC_THE2: 92;

      end;

      hence (X \/ {p}) |- q implies X |- (p1 => q);

      now

        assume X |- (p1 => q);

        then (X \/ {p1}) |- q by Th40;

        then

         A4: (X \/ {p1}) |- {q} by Th10;

        p |-| p1 by A1, Th38;

        then {p} |-| {p1} by Th29;

        then (X \/ {p}) |- {q} by A4, Th26;

        hence (X \/ {p}) |- q by Th10;

      end;

      hence thesis;

    end;

    theorem :: CQC_THE3:43



     Th43: p is closed & p |- q implies ( 'not' q) |- ( 'not' p)

    proof

      assume that

       A1: p is closed and

       A2: p |- q;

      (p => q) is valid by A1, A2, Th41;

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

      hence thesis by Th39;

    end;

    theorem :: CQC_THE3:44

    p is closed & (X \/ {p}) |- q implies (X \/ {( 'not' q)}) |- ( 'not' p)

    proof

      assume that

       A1: p is closed and

       A2: (X \/ {p}) |- q;

      X |- (p => q) by A1, A2, CQC_THE2: 92;

      then X |- (( 'not' q) => ( 'not' p)) by LUKASI_1: 69;

      hence thesis by Th40;

    end;

    theorem :: CQC_THE3:45



     Th45: p is closed & ( 'not' p) |- ( 'not' q) implies q |- p

    proof

      assume that

       A1: p is closed and

       A2: ( 'not' p) |- ( 'not' q);

      ( 'not' p) is closed by A1, QC_LANG3: 21;

      then (( 'not' p) => ( 'not' q)) is valid by A2, Th41;

      then (q => p) is valid by LUKASI_1: 52;

      hence thesis by Th39;

    end;

    theorem :: CQC_THE3:46

    p is closed & (X \/ {( 'not' p)}) |- ( 'not' q) implies (X \/ {q}) |- p

    proof

      assume that

       A1: p is closed and

       A2: (X \/ {( 'not' p)}) |- ( 'not' q);

      ( 'not' p) is closed by A1, QC_LANG3: 21;

      then X |- (( 'not' p) => ( 'not' q)) by A2, CQC_THE2: 92;

      then X |- (q => p) by LUKASI_1: 69;

      hence thesis by Th40;

    end;

    theorem :: CQC_THE3:47

    p is closed & q is closed implies (p |- q iff ( 'not' q) |- ( 'not' p)) by Th43, Th45;

    theorem :: CQC_THE3:48



     Th48: p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies (p |- q iff ( 'not' q1) |- ( 'not' p1))

    proof

      assume that

       A1: p1 is_an_universal_closure_of p and

       A2: q1 is_an_universal_closure_of q;

      now

        q |-| q1 by A2, Th38;

        then

         A3: q |- q1;

        p1 |-| p by A1, Th38;

        then

         A4: p1 |- p;

        assume p |- q;

        then p1 |- q by A4, Th6;

        then

         A5: p1 |- q1 by A3, Th6;

        p1 is closed by A1;

        hence ( 'not' q1) |- ( 'not' p1) by A5, Th43;

      end;

      hence p |- q implies ( 'not' q1) |- ( 'not' p1);

      now

        q1 |-| q by A2, Th38;

        then

         A6: q1 |- q;

        p1 |-| p by A1, Th38;

        then

         A7: p |- p1;

        assume

         A8: ( 'not' q1) |- ( 'not' p1);

        q1 is closed by A2;

        then p1 |- q1 by A8, Th45;

        then p |- q1 by A7, Th6;

        hence p |- q by A6, Th6;

      end;

      hence thesis;

    end;

    theorem :: CQC_THE3:49

    p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies (p |-| q iff ( 'not' p1) |-| ( 'not' q1)) by Th48;

    definition

      let A;

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

      :: CQC_THE3:def7

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

      reflexivity

      proof

        let p;

        ( {} ( CQC-WFF A)) |- (p => p) by CQC_THE1:def 9;

        then ( {} ( CQC-WFF A)) |- ((p => p) '&' (p => p)) by Lm2;

        then ((p => p) '&' (p => p)) is valid by CQC_THE1:def 9;

        hence thesis by QC_LANG2:def 4;

      end;

      symmetry

      proof

        let p, q;

        assume (p <=> q) is valid;

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

        then

         A1: ( {} ( CQC-WFF A)) |- ((p => q) '&' (q => p)) by CQC_THE1:def 9;

        then

         A2: ( {} ( CQC-WFF A)) |- (q => p) by Lm3;

        ( {} ( CQC-WFF A)) |- (p => q) by A1, Lm3;

        then ( {} ( CQC-WFF A)) |- ((q => p) '&' (p => q)) by A2, Lm2;

        then ((q => p) '&' (p => q)) is valid by CQC_THE1:def 9;

        hence thesis by QC_LANG2:def 4;

      end;

    end

    theorem :: CQC_THE3:50



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

    proof

       A1:

      now

        assume that

         A2: (p => q) is valid and

         A3: (q => p) is valid;



         A4: ( {} ( CQC-WFF A)) |- (q => p) by A3, CQC_THE1:def 9;

        ( {} ( CQC-WFF A)) |- (p => q) by A2, CQC_THE1:def 9;

        then ( {} ( CQC-WFF A)) |- ((p => q) '&' (q => p)) by A4, Lm2;

        then ((p => q) '&' (q => p)) is valid by CQC_THE1:def 9;

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

        hence p <==> q;

      end;

      now

        assume p <==> q;

        then (p <=> q) is valid;

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

        then

         A5: ( {} ( CQC-WFF A)) |- ((p => q) '&' (q => p)) by CQC_THE1:def 9;

        then

         A6: ( {} ( CQC-WFF A)) |- (q => p) by Lm3;

        ( {} ( CQC-WFF A)) |- (p => q) by A5, Lm3;

        hence (p => q) is valid & (q => p) is valid by A6, CQC_THE1:def 9;

      end;

      hence thesis by A1;

    end;

    theorem :: CQC_THE3:51

    p <==> q & q <==> r implies p <==> r

    proof

      assume that

       A1: p <==> q and

       A2: q <==> r;



       A3: (r => q) is valid by A2, Th50;

      (q => p) is valid by A1, Th50;

      then

       A4: (r => p) is valid by A3, LUKASI_1: 42;



       A5: (q => r) is valid by A2, Th50;

      (p => q) is valid by A1, Th50;

      then (p => r) is valid by A5, LUKASI_1: 42;

      hence thesis by A4, Th50;

    end;

    theorem :: CQC_THE3:52

    p <==> q implies p |-| q

    proof

      assume p <==> q;

      then (p <=> q) is valid;

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

      then

       A1: ( {} ( CQC-WFF A)) |- ((p => q) '&' (q => p)) by CQC_THE1:def 9;

      then ( {} ( CQC-WFF A)) |- (q => p) by Lm3;

      then

       A2: (q => p) is valid by CQC_THE1:def 9;

      ( {} ( CQC-WFF A)) |- (p => q) by A1, Lm3;

      then (p => q) is valid by CQC_THE1:def 9;

      hence p |- q & q |- p by A2, Th39;

    end;



     Lm5: p <==> q implies ( 'not' p) <==> ( 'not' q)

    proof

      assume

       A1: p <==> q;

      then (q => p) is valid by Th50;

      then

       A2: (( 'not' p) => ( 'not' q)) is valid by LUKASI_1: 52;

      (p => q) is valid by A1, Th50;

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

      hence thesis by A2, Th50;

    end;



     Lm6: ( 'not' p) <==> ( 'not' q) implies p <==> q

    proof

      assume

       A1: ( 'not' p) <==> ( 'not' q);

      then (( 'not' q) => ( 'not' p)) is valid by Th50;

      then

       A2: (p => q) is valid by LUKASI_1: 52;

      (( 'not' p) => ( 'not' q)) is valid by A1, Th50;

      then (q => p) is valid by LUKASI_1: 52;

      hence thesis by A2, Th50;

    end;

    theorem :: CQC_THE3:53

    p <==> q iff ( 'not' p) <==> ( 'not' q) by Lm5, Lm6;

    theorem :: CQC_THE3:54



     Th54: p <==> q & r <==> s implies (p '&' r) <==> (q '&' s)

    proof

      assume that

       A1: p <==> q and

       A2: r <==> s;

      (s => r) is valid by A2, Th50;

      then

       A3: (s => r) in ( TAUT A) by CQC_THE1:def 10;

      (q => p) is valid by A1, Th50;

      then (q => p) in ( TAUT A) by CQC_THE1:def 10;

      then ((q '&' s) => (p '&' r)) in ( TAUT A) by A3, PROCAL_1: 56;

      then

       A4: ((q '&' s) => (p '&' r)) is valid by CQC_THE1:def 10;

      (r => s) is valid by A2, Th50;

      then

       A5: (r => s) in ( TAUT A) by CQC_THE1:def 10;

      (p => q) is valid by A1, Th50;

      then (p => q) in ( TAUT A) by CQC_THE1:def 10;

      then ((p '&' r) => (q '&' s)) in ( TAUT A) by A5, PROCAL_1: 56;

      then ((p '&' r) => (q '&' s)) is valid by CQC_THE1:def 10;

      hence thesis by A4, Th50;

    end;

    theorem :: CQC_THE3:55



     Th55: p <==> q & r <==> s implies (p => r) <==> (q => s)

    proof

      assume that

       A1: p <==> q and

       A2: r <==> s;

      ( 'not' r) <==> ( 'not' s) by A2, Lm5;

      then (p '&' ( 'not' r)) <==> (q '&' ( 'not' s)) by A1, Th54;

      then

       A3: ( 'not' (p '&' ( 'not' r))) <==> ( 'not' (q '&' ( 'not' s))) by Lm5;

      (p => r) = ( 'not' (p '&' ( 'not' r))) by QC_LANG2:def 2;

      hence thesis by A3, QC_LANG2:def 2;

    end;

    theorem :: CQC_THE3:56

    p <==> q & r <==> s implies (p 'or' r) <==> (q 'or' s)

    proof

      assume that

       A1: p <==> q and

       A2: r <==> s;

      (s => r) is valid by A2, Th50;

      then

       A3: (s => r) in ( TAUT A) by CQC_THE1:def 10;

      (q => p) is valid by A1, Th50;

      then (q => p) in ( TAUT A) by CQC_THE1:def 10;

      then ((q 'or' s) => (p 'or' r)) in ( TAUT A) by A3, PROCAL_1: 57;

      then

       A4: ((q 'or' s) => (p 'or' r)) is valid by CQC_THE1:def 10;

      (r => s) is valid by A2, Th50;

      then

       A5: (r => s) in ( TAUT A) by CQC_THE1:def 10;

      (p => q) is valid by A1, Th50;

      then (p => q) in ( TAUT A) by CQC_THE1:def 10;

      then ((p 'or' r) => (q 'or' s)) in ( TAUT A) by A5, PROCAL_1: 57;

      then ((p 'or' r) => (q 'or' s)) is valid by CQC_THE1:def 10;

      hence thesis by A4, Th50;

    end;

    theorem :: CQC_THE3:57

    p <==> q & r <==> s implies (p <=> r) <==> (q <=> s)

    proof

      assume that

       A1: p <==> q and

       A2: r <==> s;



       A3: (r => p) <==> (s => q) by A1, A2, Th55;



       A4: (p <=> r) = ((p => r) '&' (r => p)) by QC_LANG2:def 4;

      (p => r) <==> (q => s) by A1, A2, Th55;

      then ((p => r) '&' (r => p)) <==> ((q => s) '&' (s => q)) by A3, Th54;

      hence thesis by A4, QC_LANG2:def 4;

    end;

    theorem :: CQC_THE3:58



     Th58: p <==> q implies ( All (x,p)) <==> ( All (x,q))

    proof

      assume

       A1: p <==> q;

      then (q => p) is valid by Th50;

      then ( All (x,(q => p))) is valid by CQC_THE2: 23;

      then

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

      (p => q) is valid by A1, Th50;

      then ( All (x,(p => q))) is valid by CQC_THE2: 23;

      then (( All (x,p)) => ( All (x,q))) is valid by CQC_THE2: 31;

      hence thesis by A2, Th50;

    end;

    theorem :: CQC_THE3:59

    p <==> q implies ( Ex (x,p)) <==> ( Ex (x,q))

    proof

      assume p <==> q;

      then ( 'not' p) <==> ( 'not' q) by Lm5;

      then ( All (x,( 'not' p))) <==> ( All (x,( 'not' q))) by Th58;

      then

       A1: ( 'not' ( All (x,( 'not' p)))) <==> ( 'not' ( All (x,( 'not' q)))) by Lm5;

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

      hence thesis by A1, QC_LANG2:def 5;

    end;

    theorem :: CQC_THE3:60



     Th60: for k be Nat, l be QC-variable_list of k, A, a be free_QC-variable of A, x be bound_QC-variable of A holds ( still_not-bound_in l) c= ( still_not-bound_in ( Subst (l,(a .--> x))))

    proof

      let k be Nat, l be QC-variable_list of k, A, a be free_QC-variable of A, x be bound_QC-variable of A;

      let y be object;



       A1: ( still_not-bound_in l) = { (l . n) where n be Nat : 1 <= n & n <= ( len l) & (l . n) in ( bound_QC-variables A) } by QC_LANG1:def 29;

      assume

       A2: y in ( still_not-bound_in l);

      then

      reconsider y9 = y as Element of ( still_not-bound_in l);



       A3: ( still_not-bound_in ( Subst (l,(a .--> x)))) = { (( Subst (l,(a .--> x))) . n) where n be Nat : 1 <= n & n <= ( len ( Subst (l,(a .--> x)))) & (( Subst (l,(a .--> x))) . n) in ( bound_QC-variables A) } by QC_LANG1:def 29;

      consider n be Nat such that

       A4: y9 = (l . n) and

       A5: 1 <= n and

       A6: n <= ( len l) and

       A7: (l . n) in ( bound_QC-variables A) by A1, A2;

      (l . n) <> a by A7, QC_LANG3: 34;

      then

       A8: (l . n) = (( Subst (l,(a .--> x))) . n) by A5, A6, CQC_LANG: 3;

      n <= ( len ( Subst (l,(a .--> x)))) by A6, CQC_LANG:def 1;

      hence y in ( still_not-bound_in ( Subst (l,(a .--> x)))) by A3, A4, A5, A7, A8;

    end;

    theorem :: CQC_THE3:61



     Th61: for k be Nat, l be QC-variable_list of k, A, a be free_QC-variable of A, x be bound_QC-variable of A holds ( still_not-bound_in ( Subst (l,(a .--> x)))) c= (( still_not-bound_in l) \/ {x})

    proof

      let k be Nat, l be QC-variable_list of k, A, a be free_QC-variable of A, x be bound_QC-variable of A;

      let y be object;



       A1: ( still_not-bound_in l) = { (l . n) where n be Nat : 1 <= n & n <= ( len l) & (l . n) in ( bound_QC-variables A) } by QC_LANG1:def 29;

      assume

       A2: y in ( still_not-bound_in ( Subst (l,(a .--> x))));

      then

      reconsider y9 = y as Element of ( still_not-bound_in ( Subst (l,(a .--> x))));

      ( still_not-bound_in ( Subst (l,(a .--> x)))) = { (( Subst (l,(a .--> x))) . n) where n be Nat : 1 <= n & n <= ( len ( Subst (l,(a .--> x)))) & (( Subst (l,(a .--> x))) . n) in ( bound_QC-variables A) } by QC_LANG1:def 29;

      then

      consider n be Nat such that

       A3: y9 = (( Subst (l,(a .--> x))) . n) and

       A4: 1 <= n and

       A5: n <= ( len ( Subst (l,(a .--> x)))) and

       A6: (( Subst (l,(a .--> x))) . n) in ( bound_QC-variables A) by A2;



       A7: n <= ( len l) by A5, CQC_LANG:def 1;

      per cases ;

        suppose (l . n) = a;

        then y9 = x by A3, A4, A7, CQC_LANG: 3;

        then y9 in {x} by TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose (l . n) <> a;

        then (l . n) = (( Subst (l,(a .--> x))) . n) by A4, A7, CQC_LANG: 3;

        then y9 in ( still_not-bound_in l) by A1, A3, A4, A6, A7;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: CQC_THE3:62



     Th62: for h holds ( still_not-bound_in h) c= ( still_not-bound_in (h . x))

    proof

      defpred P[ QC-formula of A] means ( still_not-bound_in $1) c= ( still_not-bound_in ($1 . x));



       A1: for p be Element of ( QC-WFF A) st P[p] holds P[( 'not' p)]

      proof

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

        ( still_not-bound_in (( 'not' p) . x)) = ( still_not-bound_in ( 'not' (p . x))) by CQC_LANG: 19

        .= ( still_not-bound_in (p . x)) by QC_LANG3: 7;

        hence thesis by QC_LANG3: 7;

      end;



       A2: for p,q be Element of ( QC-WFF A) st P[p] & P[q] holds P[(p '&' q)]

      proof

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

         A3: P[p] and

         A4: P[q];



         A5: ( still_not-bound_in ((p '&' q) . x)) = ( still_not-bound_in ((p . x) '&' (q . x))) by CQC_LANG: 21

        .= (( still_not-bound_in (p . x)) \/ ( still_not-bound_in (q . x))) by QC_LANG3: 10;

        ( still_not-bound_in (p '&' q)) = (( still_not-bound_in p) \/ ( still_not-bound_in q)) by QC_LANG3: 10;

        hence thesis by A3, A4, A5, XBOOLE_1: 13;

      end;



       A6: for x be bound_QC-variable of A, p be Element of ( QC-WFF A) st P[p] holds P[( All (x,p))]

      proof

        let y be bound_QC-variable of A, p be Element of ( QC-WFF A) such that

         A7: P[p];

        per cases ;

          suppose y = x;

          hence thesis by CQC_LANG: 24;

        end;

          suppose

           A8: y <> x;



           A9: ( still_not-bound_in ( All (y,p))) = (( still_not-bound_in p) \ {y}) by QC_LANG3: 12;

          ( still_not-bound_in (( All (y,p)) . x)) = ( still_not-bound_in ( All (y,(p . x)))) by A8, CQC_LANG: 25

          .= (( still_not-bound_in (p . x)) \ {y}) by QC_LANG3: 12;

          hence thesis by A7, A9, XBOOLE_1: 33;

        end;

      end;



       A10: for k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A holds P[(P ! ll)]

      proof

        let k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A;



         A11: ( still_not-bound_in ((P ! ll) . x)) = ( still_not-bound_in (P ! ( Subst (ll,((A a. 0 ) .--> x))))) by CQC_LANG: 17

        .= ( still_not-bound_in ( Subst (ll,((A a. 0 ) .--> x)))) by QC_LANG3: 5;

        ( still_not-bound_in ll) c= ( still_not-bound_in ( Subst (ll,((A a. 0 ) .--> x)))) by Th60;

        hence thesis by A11, QC_LANG3: 5;

      end;



       A12: P[( VERUM A)] by CQC_LANG: 15;

      thus for h holds P[h] from QC_LANG1:sch 1( A10, A12, A1, A2, A6);

    end;

    theorem :: CQC_THE3:63



     Th63: for h holds ( still_not-bound_in (h . x)) c= (( still_not-bound_in h) \/ {x})

    proof

      defpred P[ QC-formula of A] means ( still_not-bound_in ($1 . x)) c= (( still_not-bound_in $1) \/ {x});



       A1: for p be Element of ( QC-WFF A) st P[p] holds P[( 'not' p)]

      proof

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

        ( still_not-bound_in (( 'not' p) . x)) = ( still_not-bound_in ( 'not' (p . x))) by CQC_LANG: 19

        .= ( still_not-bound_in (p . x)) by QC_LANG3: 7;

        hence thesis by QC_LANG3: 7;

      end;



       A2: for p,q be Element of ( QC-WFF A) st P[p] & P[q] holds P[(p '&' q)]

      proof

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

         A3: P[p] and

         A4: P[q];



         A5: ( still_not-bound_in ((p '&' q) . x)) = ( still_not-bound_in ((p . x) '&' (q . x))) by CQC_LANG: 21

        .= (( still_not-bound_in (p . x)) \/ ( still_not-bound_in (q . x))) by QC_LANG3: 10;



         A6: ((( still_not-bound_in p) \/ {x}) \/ (( still_not-bound_in q) \/ {x})) = ((( still_not-bound_in p) \/ ( {x} \/ ( still_not-bound_in q))) \/ {x}) by XBOOLE_1: 4

        .= (((( still_not-bound_in p) \/ ( still_not-bound_in q)) \/ {x}) \/ {x}) by XBOOLE_1: 4

        .= ((( still_not-bound_in p) \/ ( still_not-bound_in q)) \/ ( {x} \/ {x})) by XBOOLE_1: 4

        .= ((( still_not-bound_in p) \/ ( still_not-bound_in q)) \/ {x});

        (( still_not-bound_in (p . x)) \/ ( still_not-bound_in (q . x))) c= ((( still_not-bound_in p) \/ {x}) \/ (( still_not-bound_in q) \/ {x})) by A3, A4, XBOOLE_1: 13;

        hence thesis by A5, A6, QC_LANG3: 10;

      end;



       A7: for x be bound_QC-variable of A, p be Element of ( QC-WFF A) st P[p] holds P[( All (x,p))]

      proof

        let y be bound_QC-variable of A, p be Element of ( QC-WFF A) such that

         A8: P[p];

        per cases ;

          suppose

           A9: y = x;



           A10: (( still_not-bound_in p) \ {x}) c= ( still_not-bound_in p) by XBOOLE_1: 36;



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

          ( still_not-bound_in p) c= ( still_not-bound_in (p . x)) by Th62;

          then ( still_not-bound_in ( All (x,p))) c= ( still_not-bound_in (p . x)) by A11, A10;

          then

           A12: ( still_not-bound_in ( All (x,p))) c= (( still_not-bound_in p) \/ {x}) by A8, XBOOLE_1: 1;

          (( still_not-bound_in ( All (y,p))) \/ {x}) = ((( still_not-bound_in p) \ {x}) \/ {x}) by A9, QC_LANG3: 12

          .= (( still_not-bound_in p) \/ {x}) by XBOOLE_1: 39;

          hence thesis by A9, A12, CQC_LANG: 24;

        end;

          suppose

           A13: y <> x;



           A14: (( still_not-bound_in ( All (y,p))) \/ {x}) = ((( still_not-bound_in p) \ {y}) \/ {x}) by QC_LANG3: 12

          .= ((( still_not-bound_in p) \/ {x}) \ {y}) by A13, XBOOLE_1: 87, ZFMISC_1: 11;

          ( still_not-bound_in (( All (y,p)) . x)) = ( still_not-bound_in ( All (y,(p . x)))) by A13, CQC_LANG: 25

          .= (( still_not-bound_in (p . x)) \ {y}) by QC_LANG3: 12;

          hence thesis by A8, A14, XBOOLE_1: 33;

        end;

      end;



       A15: for k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A holds P[(P ! ll)]

      proof

        let k be Nat, P be QC-pred_symbol of k, A, ll be QC-variable_list of k, A;



         A16: ( still_not-bound_in ((P ! ll) . x)) = ( still_not-bound_in (P ! ( Subst (ll,((A a. 0 ) .--> x))))) by CQC_LANG: 17

        .= ( still_not-bound_in ( Subst (ll,((A a. 0 ) .--> x)))) by QC_LANG3: 5;

        ( still_not-bound_in ( Subst (ll,((A a. 0 ) .--> x)))) c= (( still_not-bound_in ll) \/ {x}) by Th61;

        hence thesis by A16, QC_LANG3: 5;

      end;



       A17: ( still_not-bound_in ( VERUM A)) = {} by QC_LANG3: 3;

      (( VERUM A) . x) = ( VERUM A) by CQC_LANG: 15;

      then ( still_not-bound_in (( VERUM A) . x)) = {} by A17;

      then

       A18: ( still_not-bound_in (( VERUM A) . x)) c= (( still_not-bound_in ( VERUM A)) \/ {x}) by XBOOLE_1: 2;



       A19: P[( VERUM A)] by A18;

      thus for h holds P[h] from QC_LANG1:sch 1( A15, A19, A1, A2, A7);

    end;

    theorem :: CQC_THE3:64



     Th64: p = (h . x) & x <> y & not y in ( still_not-bound_in h) implies not y in ( still_not-bound_in p)

    proof

      assume that

       A1: p = (h . x) and

       A2: x <> y and

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

       A4: y in ( still_not-bound_in p);



       A5: ( still_not-bound_in p) c= (( still_not-bound_in h) \/ {x}) by A1, Th63;

      per cases by A4, A5, XBOOLE_0:def 3;

        suppose y in ( still_not-bound_in h);

        hence contradiction by A3;

      end;

        suppose y in {x};

        hence contradiction by A2, TARSKI:def 1;

      end;

    end;

    theorem :: CQC_THE3:65

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

    proof

      assume that

       A1: p = (h . x) and

       A2: q = (h . y) and

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

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

      per cases ;

        suppose x = y;

        hence thesis by A1, A2;

      end;

        suppose

         A5: x <> y;

        then not x in ( still_not-bound_in q) by A2, A3, Th64;

        then

         A6: (( All (y,q)) => ( All (x,p))) is valid by A1, A2, A4, CQC_THE2: 27;

         not y in ( still_not-bound_in p) by A1, A4, A5, Th64;

        then (( All (x,p)) => ( All (y,q))) is valid by A1, A2, A3, CQC_THE2: 27;

        hence thesis by A6, Th50;

      end;

    end;