let n be non empty Nat; :: thesis: for J being non empty non void Signature

for T being non-empty MSAlgebra over J

for X being V3() GeneratorSet of T

for S1 being non empty non void b_{1} -extension n PC-correct QC-correct QCLangSignature over Union X

for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let J be non empty non void Signature; :: thesis: for T being non-empty MSAlgebra over J

for X being V3() GeneratorSet of T

for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let T be non-empty MSAlgebra over J; :: thesis: for X being V3() GeneratorSet of T

for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let X be V3() GeneratorSet of T; :: thesis: for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let S1 be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X; :: thesis: for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let L be non-empty Language of X extended_by ({}, the carrier of S1),S1; :: thesis: for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let G be QC-theory of L; :: thesis: for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let A, B be Formula of L; :: thesis: for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let x be Element of Union X; :: thesis: ( L is subst-correct & L is vf-qc-correct & A \iff B in G implies (\for (x,A)) \iff (\for (x,B)) in G )

assume A1: ( L is subst-correct & L is vf-qc-correct ) ; :: thesis: ( not A \iff B in G or (\for (x,A)) \iff (\for (x,B)) in G )

set p = A \imp B;

set q = B \imp A;

set pq = A \iff B;

set a = \for (x,(A \iff B));

set b = \for (x,(A \imp B));

set c = (\for (x,A)) \imp (\for (x,B));

(A \iff B) \imp (A \imp B) in G by Def38;

then A2: (\for (x,(A \iff B))) \imp (\for (x,(A \imp B))) in G by A1, Th115;

(\for (x,(A \imp B))) \imp ((\for (x,A)) \imp (\for (x,B))) in G by A1, Th109;

then A3: (\for (x,(A \iff B))) \imp ((\for (x,A)) \imp (\for (x,B))) in G by A2, Th45;

(A \iff B) \imp (B \imp A) in G by Def38;

then A4: (\for (x,(A \iff B))) \imp (\for (x,(B \imp A))) in G by A1, Th115;

(\for (x,(B \imp A))) \imp ((\for (x,B)) \imp (\for (x,A))) in G by A1, Th109;

then A5: (\for (x,(A \iff B))) \imp ((\for (x,B)) \imp (\for (x,A))) in G by A4, Th45;

((\for (x,(A \iff B))) \imp ((\for (x,A)) \imp (\for (x,B)))) \imp (((\for (x,(A \iff B))) \imp ((\for (x,B)) \imp (\for (x,A)))) \imp ((\for (x,(A \iff B))) \imp (((\for (x,A)) \imp (\for (x,B))) \and ((\for (x,B)) \imp (\for (x,A)))))) in G by Th49;

then ((\for (x,(A \iff B))) \imp ((\for (x,B)) \imp (\for (x,A)))) \imp ((\for (x,(A \iff B))) \imp (((\for (x,A)) \imp (\for (x,B))) \and ((\for (x,B)) \imp (\for (x,A))))) in G by A3, Def38;

then A6: (\for (x,(A \iff B))) \imp (((\for (x,A)) \imp (\for (x,B))) \and ((\for (x,B)) \imp (\for (x,A)))) in G by A5, Def38;

(((\for (x,A)) \imp (\for (x,B))) \and ((\for (x,B)) \imp (\for (x,A)))) \imp ((\for (x,A)) \iff (\for (x,B))) in G by Def38;

then A7: (\for (x,(A \iff B))) \imp ((\for (x,A)) \iff (\for (x,B))) in G by A6, Th45;

assume A \iff B in G ; :: thesis: (\for (x,A)) \iff (\for (x,B)) in G

then \for (x,(A \iff B)) in G by Def39;

hence (\for (x,A)) \iff (\for (x,B)) in G by A7, Def38; :: thesis: verum

for T being non-empty MSAlgebra over J

for X being V3() GeneratorSet of T

for S1 being non empty non void b

for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let J be non empty non void Signature; :: thesis: for T being non-empty MSAlgebra over J

for X being V3() GeneratorSet of T

for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let T be non-empty MSAlgebra over J; :: thesis: for X being V3() GeneratorSet of T

for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let X be V3() GeneratorSet of T; :: thesis: for S1 being non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X

for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let S1 be non empty non void J -extension n PC-correct QC-correct QCLangSignature over Union X; :: thesis: for L being non-empty Language of X extended_by ({}, the carrier of S1),S1

for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let L be non-empty Language of X extended_by ({}, the carrier of S1),S1; :: thesis: for G being QC-theory of L

for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let G be QC-theory of L; :: thesis: for A, B being Formula of L

for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let A, B be Formula of L; :: thesis: for x being Element of Union X st L is subst-correct & L is vf-qc-correct & A \iff B in G holds

(\for (x,A)) \iff (\for (x,B)) in G

let x be Element of Union X; :: thesis: ( L is subst-correct & L is vf-qc-correct & A \iff B in G implies (\for (x,A)) \iff (\for (x,B)) in G )

assume A1: ( L is subst-correct & L is vf-qc-correct ) ; :: thesis: ( not A \iff B in G or (\for (x,A)) \iff (\for (x,B)) in G )

set p = A \imp B;

set q = B \imp A;

set pq = A \iff B;

set a = \for (x,(A \iff B));

set b = \for (x,(A \imp B));

set c = (\for (x,A)) \imp (\for (x,B));

(A \iff B) \imp (A \imp B) in G by Def38;

then A2: (\for (x,(A \iff B))) \imp (\for (x,(A \imp B))) in G by A1, Th115;

(\for (x,(A \imp B))) \imp ((\for (x,A)) \imp (\for (x,B))) in G by A1, Th109;

then A3: (\for (x,(A \iff B))) \imp ((\for (x,A)) \imp (\for (x,B))) in G by A2, Th45;

(A \iff B) \imp (B \imp A) in G by Def38;

then A4: (\for (x,(A \iff B))) \imp (\for (x,(B \imp A))) in G by A1, Th115;

(\for (x,(B \imp A))) \imp ((\for (x,B)) \imp (\for (x,A))) in G by A1, Th109;

then A5: (\for (x,(A \iff B))) \imp ((\for (x,B)) \imp (\for (x,A))) in G by A4, Th45;

((\for (x,(A \iff B))) \imp ((\for (x,A)) \imp (\for (x,B)))) \imp (((\for (x,(A \iff B))) \imp ((\for (x,B)) \imp (\for (x,A)))) \imp ((\for (x,(A \iff B))) \imp (((\for (x,A)) \imp (\for (x,B))) \and ((\for (x,B)) \imp (\for (x,A)))))) in G by Th49;

then ((\for (x,(A \iff B))) \imp ((\for (x,B)) \imp (\for (x,A)))) \imp ((\for (x,(A \iff B))) \imp (((\for (x,A)) \imp (\for (x,B))) \and ((\for (x,B)) \imp (\for (x,A))))) in G by A3, Def38;

then A6: (\for (x,(A \iff B))) \imp (((\for (x,A)) \imp (\for (x,B))) \and ((\for (x,B)) \imp (\for (x,A)))) in G by A5, Def38;

(((\for (x,A)) \imp (\for (x,B))) \and ((\for (x,B)) \imp (\for (x,A)))) \imp ((\for (x,A)) \iff (\for (x,B))) in G by Def38;

then A7: (\for (x,(A \iff B))) \imp ((\for (x,A)) \iff (\for (x,B))) in G by A6, Th45;

assume A \iff B in G ; :: thesis: (\for (x,A)) \iff (\for (x,B)) in G

then \for (x,(A \iff B)) in G by Def39;

hence (\for (x,A)) \iff (\for (x,B)) in G by A7, Def38; :: thesis: verum