:: Logical Equivalence of Formulae
::  by Oleg Okhotnikov
::
:: Received January 24, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, CQC_THE1, TARSKI,
      XBOOLE_0, XBOOLEAN, BVFUNC_2, RCOMP_1, XXREAL_0, FINSEQ_1, FUNCT_1,
      ARYTM_3, CARD_1, ZFREFLE1, FUNCOP_1, REALSET1, QC_LANG3, CQC_THE3;
 notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, NUMBERS, ORDINAL1, NAT_1,
      FUNCT_1, FINSEQ_1, QC_LANG1, QC_LANG3, CQC_LANG, CQC_THE1, XXREAL_0;
 constructors DOMAIN_1, XXREAL_0, NAT_1, MEMBERED, QC_LANG3, CQC_THE1;
 registrations SUBSET_1, RELSET_1, MEMBERED, CQC_LANG, LUKASI_1, RELAT_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI;
 theorems TARSKI, ZFMISC_1, SUBSET_1, CQC_THE1, CQC_THE2, LUKASI_1, NAT_1,
      QC_LANG1, QC_LANG2, QC_LANG3, PROCAL_1, CQC_LANG, XBOOLE_0, XBOOLE_1;
 schemes NAT_1, QC_LANG1;

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 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 Th2:
  X c= Cn(Y) implies Cn(X) c= Cn(Y) by CQC_THE1:15,16;

theorem 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,16;
  q in Cn({p}) by A2,CQC_THE1:def 8;
  hence thesis by A3,CQC_THE1:def 8;
end;

theorem 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);
  pred p |- q means
  :Def1:
  {p} |- q;
end;

theorem Th5:
  p |- p
proof
  {p} |- p by CQC_THE2:87;
  hence thesis by Def1;
end;

theorem Th6:
  p |- q & q |- r implies p |- r
proof
  assume that
A1: p |- q and
A2: q |- r;
A3: {q} |- r by A2,Def1;
  {p} |- q by A1,Def1;
  then {p} |- r by A3,Th3;
  hence thesis by Def1;
end;

definition
  let A;
  let X, Y be Subset of CQC-WFF(A);
  pred X |- Y means
  :Def2:
  for p being Element of CQC-WFF(A) st p in Y holds X |- p;
end;

theorem Th7:
  X |- Y iff Y c= Cn(X)
proof
A1: now
    assume
A2: X |- Y;
    now
      let p be set;
      assume
A3:   p in Y;
      then reconsider p9 = p as Element of CQC-WFF(A);
      X |- p9 by A2,A3,Def2;
      hence p in Cn(X) by CQC_THE1:def 8;
    end;
    hence Y c= Cn(X) by TARSKI:def 3;
  end;
  now
    assume Y c= Cn(X);
    then for p st p in Y holds X |- p by CQC_THE1:def 8;
    hence X |- Y by Def2;
  end;
  hence thesis by A1;
end;

theorem
  X |- X
proof
  for p st p in X holds X |- p by Th1;
  hence thesis by Def2;
end;

theorem 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,Def2;
    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,16;
    hence thesis by A3,CQC_THE1:def 8;
  end;
  hence thesis by Def2;
end;

theorem Th10:
  X |- {p} iff X |- p
proof
A1: now
    assume X |- p;
    then for q st q in {p} holds X |- q by TARSKI:def 1;
    hence X |- {p} by Def2;
  end;
  now
A2: p in {p} by TARSKI:def 1;
    assume X |- {p};
    hence X |- p by A2,Def2;
  end;
  hence thesis by A1;
end;

theorem Th11:
  {p} |- {q} iff p |- q
proof
A1: now
    assume p |- q;
    then {p} |- q by Def1;
    hence {p} |- {q} by Th10;
  end;
  now
    assume {p} |- {q};
    then {p} |- q by Th10;
    hence p |- q by Def1;
  end;
  hence thesis by A1;
end;

theorem
  X c= Y implies Y |- X
proof
  assume X c= Y;
  then for p st p in X holds Y |- p by Th1;
  hence thesis by Def2;
end;

theorem Th13:
  X |- TAUT(A)
proof
  TAUT(A) c= Cn(X) by CQC_THE1:39;
  hence thesis by Th7;
end;

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

definition
  let A;
  let X be Subset of CQC-WFF(A);
  pred |- X means
  :Def3:
  for p being Element of CQC-WFF(A) st p in X holds p is valid;
end;

theorem Th15:
  |- X iff {}(CQC-WFF(A)) |- X
proof
A1: now
    assume
A2: {}(CQC-WFF(A)) |- X;
    now
      let p;
      assume p in X;
      then {}(CQC-WFF(A)) |- p by A2,Def2;
      hence p is valid by CQC_THE1:def 9;
    end;
    hence |- X by Def3;
  end;
  now
    assume
A3: |- X;
    now
      let p;
      assume p in X;
      then p is valid by A3,Def3;
      hence {}(CQC-WFF(A)) |- p by CQC_THE1:def 9;
    end;
    hence {}(CQC-WFF(A)) |- X by Def2;
  end;
  hence thesis by A1;
end;

theorem
  |- 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
  |- X iff X c= TAUT(A)
proof
A1: now
    assume
A2: |- X;
    now
      let p;
      assume p in X;
      then p is valid by A2,Def3;
      hence p in TAUT(A) by CQC_THE1:def 10;
    end;
    hence X c= TAUT(A) by SUBSET_1:2;
  end;
  now
    assume X c= TAUT(A);
    then for p st p in X holds p is valid by CQC_THE1:def 10;
    hence |- X by Def3;
  end;
  hence thesis by A1;
end;

definition
  let A, X, Y;
  pred X |-| Y means
  :Def4:
  for p holds (X |- p iff Y |- p);
  reflexivity;
  symmetry;
end;

theorem Th18:
  X |-| Y iff X |- Y & Y |- X
proof
A1: now
    assume that
A2: X |- Y and
A3: Y |- X;
    now
      let p;
A4:   now
        assume Y |- p;
        then Y |- {p} by Th10;
        then X |- {p} by A2,Th9;
        hence X |- p by Th10;
      end;
      now
        assume X |- p;
        then X |- {p} by Th10;
        then Y |- {p} by A3,Th9;
        hence Y |- p by Th10;
      end;
      hence X |- p iff Y |- p by A4;
    end;
    hence X |-| Y by Def4;
  end;
  now
    assume
A5: X |-| Y;
    now
      let p;
      assume p in Y;
      then Y |- p by Th1;
      hence X |- p by A5,Def4;
    end;
    hence X |- Y by Def2;
    now
      let p;
      assume p in X;
      then X |- p by Th1;
      hence Y |- p by A5,Def4;
    end;
    hence Y |- X by Def2;
  end;
  hence thesis by A1;
end;

theorem Th19:
  X |-| Y & Y |-| Z implies X |-| Z
proof
  assume that
A1: X |-| Y and
A2: Y |-| Z;
A3: Z |- Y by A2,Th18;
  Y |- X by A1,Th18;
  then
A4: Z |- X by A3,Th9;
A5: Y |- Z by A2,Th18;
  X |- Y by A1,Th18;
  then X |- Z by A5,Th9;
  hence thesis by A4,Th18;
end;

theorem 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,16;
    X |- Y by A2,Th18;
    then Y c= Cn(X) by Th7;
    then Cn(Y) c= Cn(X) by CQC_THE1:15,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 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 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
  X |-| Cn(X)
proof
  Cn(X) = Cn(Cn(X)) by CQC_THE1:19;
  hence thesis by Th20;
end;

theorem
  X \/ Y |-| Cn(X) \/ Cn(Y)
proof
  Cn(X \/ Y) = Cn(Cn(X) \/ Cn(Y)) by Th22;
  hence thesis by Th20;
end;

theorem 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 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 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);
  pred p |-| q means
  :Def5:
  p |- q & q |- p;
  reflexivity by Th5;
  symmetry;
end;

theorem Th28:
  p |-| q & q |-| r implies p |-| r
proof
  assume that
A1: p |-| q and
A2: q |-| r;
A3: r |- q by A2,Def5;
  q |- p by A1,Def5;
  then
A4: r |- p by A3,Th6;
A5: q |- r by A2,Def5;
  p |- q by A1,Def5;
  then p |- r by A5,Th6;
  hence thesis by A4,Def5;
end;

theorem 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,Def5;
  end;
  now
    assume
A4: p |-| q;
    then q |- p by Def5;
    then
A5: {q} |- {p} by Th11;
    p |- q by A4,Def5;
    then {p} |- {q} by Th11;
    hence {p} |-| {q} by A5,Th18;
  end;
  hence thesis by A1;
end;

theorem
  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 Th31:
  {p,q} |-| {p '&' q}
proof
  for r holds {p,q} |- r iff {p '&' q} |- r by CQC_THE2:89;
  hence thesis by Def4;
end;

theorem
  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,Th19;
  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} by Def2;
  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,Def2;
  q in {p,q} by TARSKI:def 2;
  hence thesis by A2,Def2;
end;

theorem
  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,Def5;
  then {r} |- s by Def1;
  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,Def5;
  then {p} |- q by Def1;
  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
  p |-| q & r |-| s implies p '&' r |-| q '&' s
proof
  assume that
A1: p |-| q and
A2: r |-| s;
A3: q '&' s |- p '&' r by A1,A2,Lm4;
  p '&' r |- q '&' s by A1,A2,Lm4;
  hence thesis by A3,Def5;
end;

theorem 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 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 by Def1;
  {p} |- p by CQC_THE2:87;
  then {p} |- All(x,p) by Th35;
  hence thesis by Def1;
end;

theorem
  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);
  pred p is_an_universal_closure_of q means
  :Def6:
  p is closed & ex n being
Element of NAT st 1 <= n & ex L being FinSequence st len L = n & L.1 = q & L.n
  = p & for k being Element of NAT st 1 <= k & k < n holds
  ex x being bound_QC-variable of A st
ex r being Element of CQC-WFF(A) st r = L.k &
L.(k+1) = All(x,r);
end;

theorem Th38:
  p is_an_universal_closure_of q implies p |-| q
proof
  assume p is_an_universal_closure_of q;
  then consider n being Element of NAT such that
A1: 1 <= n and
A2: ex L being FinSequence st len L = n & L.1 = q & L.n = p & for k
being Element of NAT st 1 <= k & k < n holds ex x, r st r = L.k & L.(k+1) = All
  (x,r) by Def6;
  consider L being FinSequence such that
  len L = n and
A3: L.1 = q and
A4: L.n = p and
A5: for k being Element of NAT st 1 <= k & k < n holds ex x, r st r = L.
  k & L.(k+1) = All(x,r) by A2;
  for k being Element of NAT st 1 <= k & k <= n ex r st r = L.k & q |-| r
  proof
    defpred P[Element of NAT] means 1 <= $1 & $1 <= n implies ex r st r = L.$1
    & q |-| r;
A6: for k being Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT such that
A7:   P[k];
      now
        assume that
        1 <= k+1 and
A8:     k+1 <= n;
        per cases by A8,NAT_1:13,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 being Element of NAT holds P[k] from NAT_1:sch 1(A14,A6 );
  end;
  then ex r st r = L.n & q |-| r by A1;
  hence thesis by A4;
end;

theorem 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 by Def1;
end;

theorem 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 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,Def1;
  then {}(CQC-WFF(A)) |- p => q by A1,CQC_THE2:92;
  hence thesis by CQC_THE1:def 9;
end;

theorem
  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,Def6;
    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 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
  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 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
  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
  p is closed & q is closed implies (p |- q iff 'not' q |- 'not' p) by Th43
,Th45;

theorem 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 by Def5;
    p1 |-| p by A1,Th38;
    then
A4: p1 |- p by Def5;
    assume p |- q;
    then p1 |- q by A4,Th6;
    then
A5: p1 |- q1 by A3,Th6;
    p1 is closed by A1,Def6;
    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 by Def5;
    p1 |-| p by A1,Th38;
    then
A7: p |- p1 by Def5;
    assume
A8: 'not' q1 |- 'not' p1;
    q1 is closed by A2,Def6;
    then p1 |- q1 by A8,Th45;
    then p |- q1 by A7,Th6;
    hence p |- q by A6,Th6;
  end;
  hence thesis;
end;

theorem
  p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q
  implies (p |-| q iff 'not' p1 |-| 'not' q1)
proof
  assume that
A1: p1 is_an_universal_closure_of p and
A2: q1 is_an_universal_closure_of q;
  now
    assume
A3: p |-| q;
    then p |- q by Def5;
    then
A4: 'not' q1 |- 'not' p1 by A1,A2,Th48;
    q |- p by A3,Def5;
    then 'not' p1 |- 'not' q1 by A1,A2,Th48;
    hence 'not' p1 |-| 'not' q1 by A4,Def5;
  end;
  hence p |-| q implies 'not' p1 |-| 'not' q1;
  now
    assume
A5: 'not' p1 |-| 'not' q1;
    then 'not' q1 |- 'not' p1 by Def5;
    then
A6: p |- q by A1,A2,Th48;
    'not' p1 |- 'not' q1 by A5,Def5;
    then q |- p by A1,A2,Th48;
    hence p |-| q by A6,Def5;
  end;
  hence thesis;
end;

definition
  let A;
  let p, q be Element of CQC-WFF(A);
  pred p <==> q means
  :Def7:
  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 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 by Def7;
  end;
  now
    assume p <==> q;
    then p <=> q is valid by Def7;
    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
  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
  p <==> q implies p |-| q
proof
  assume p <==> q;
  then p <=> q is valid by Def7;
  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
  p <==> q iff 'not' p <==> 'not' q by Lm5,Lm6;

theorem 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 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
  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
  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 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
  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 Th60:
  for k being Element of NAT, l being QC-variable_list of k,A, a
being free_QC-variable of A, x being bound_QC-variable of A holds
still_not-bound_in l c=
  still_not-bound_in Subst(l,a .--> x)
proof
  let k be Element of NAT, l be QC-variable_list of k,A,
  a be free_QC-variable of A,
  x be bound_QC-variable of A;
  now
    let y be set;
A1: still_not-bound_in l = { l.n : 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 : 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 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;
  hence thesis by TARSKI:def 3;
end;

theorem Th61:
  for k being Element of NAT, l being QC-variable_list of k,A, a
  being free_QC-variable of A,
  x being 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 Element of 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 set;
A1: still_not-bound_in l = { l.n : 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 : 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 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 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 being 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 being 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 being bound_QC-variable of A, p being 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 being Element of NAT, P being (QC-pred_symbol of k,A), ll being
  QC-variable_list of k,A holds P[P!ll]
  proof
    let k be Element of 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 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 being 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 being 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 being bound_QC-variable of A,
   p being 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,
XBOOLE_1:1;
      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 being Element of NAT, P being (QC-pred_symbol of k,A), ll being
  QC-variable_list of k,A holds P[P!ll]
  proof
    let k be Element of 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 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
  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;