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₁ -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