let n be non empty Nat; :: thesis: for S being non empty non void n PC-correct PCLangSignature
for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \iff B) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F
let S be non empty non void n PC-correct PCLangSignature ; :: thesis: for L being language MSAlgebra over S
for F being PC-theory of L
for A, B being Formula of L holds (A \iff B) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F
let L be language MSAlgebra over S; :: thesis: for F being PC-theory of L
for A, B being Formula of L holds (A \iff B) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F
let F be PC-theory of L; :: thesis: for A, B being Formula of L holds (A \iff B) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F
let A, B be Formula of L; :: thesis: (A \iff B) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F
( ((\not A) \and (A \or (\not B))) \imp ((A \or (\not B)) \and (\not A)) in F & (B \and (A \or (\not B))) \imp ((A \or (\not B)) \and B) in F ) by Th50;
then ( (((A \or (\not B)) \and (\not A)) \or ((A \or (\not B)) \and B)) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F & (((\not A) \and (A \or (\not B))) \or (B \and (A \or (\not B)))) \imp (((A \or (\not B)) \and (\not A)) \or ((A \or (\not B)) \and B)) in F ) by Th54, Th59;
then A1: (((\not A) \and (A \or (\not B))) \or (B \and (A \or (\not B)))) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F by Th45;
( (((\not A) \and A) \or ((\not A) \and (\not B))) \imp ((\not A) \and (A \or (\not B))) in F & ((B \and A) \or (B \and (\not B))) \imp (B \and (A \or (\not B))) in F & ((\not A) \and (\not B)) \imp (((\not A) \and A) \or ((\not A) \and (\not B))) in F & (B \and A) \imp ((B \and A) \or (B \and (\not B))) in F ) by Def38, Th54;
then ( ((\not A) \and (\not B)) \imp ((\not A) \and (A \or (\not B))) in F & (B \and A) \imp (B \and (A \or (\not B))) in F ) by Th45;
then (((\not A) \and (\not B)) \or (B \and A)) \imp (((\not A) \and (A \or (\not B))) \or (B \and (A \or (\not B)))) in F by Th59;
then A2: (((\not A) \and (\not B)) \or (B \and A)) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F by A1, Th45;
( (A \and B) \imp (B \and A) in F & ((\not A) \and (\not B)) \imp ((\not A) \and (\not B)) in F ) by Th34, Th50;
then ( (((\not A) \and (\not B)) \or (A \and B)) \imp (((\not A) \and (\not B)) \or (B \and A)) in F & ((A \and B) \or ((\not A) \and (\not B))) \imp (((\not A) \and (\not B)) \or (A \and B)) in F ) by Th36, Th59;
then ((A \and B) \or ((\not A) \and (\not B))) \imp (((\not A) \and (\not B)) \or (B \and A)) in F by Th45;
then A3: ((A \and B) \or ((\not A) \and (\not B))) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F by A2, Th45;
(A \iff B) \imp ((A \and B) \or ((\not A) \and (\not B))) in F by Th86;
hence (A \iff B) \imp ((A \or (\not B)) \and ((\not A) \or B)) in F by A3, Th45; :: thesis: verum