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 (B \iff A) 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 (B \iff A) 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 (B \iff A) in F

let F be PC-theory of L; :: thesis: for A, B being Formula of L holds (A \iff B) \imp (B \iff A) in F

let A, B be Formula of L; :: thesis: (A \iff B) \imp (B \iff A) in F

A1: ((B \imp A) \and (A \imp B)) \imp (B \iff A) in F by Def38;

A2: ((A \imp B) \and (B \imp A)) \imp ((B \imp A) \and (A \imp B)) in F by Th50;

(((A \imp B) \and (B \imp A)) \imp ((B \imp A) \and (A \imp B))) \imp ((((B \imp A) \and (A \imp B)) \imp (B \iff A)) \imp (((A \imp B) \and (B \imp A)) \imp (B \iff A))) in F by Th39;

then (((B \imp A) \and (A \imp B)) \imp (B \iff A)) \imp (((A \imp B) \and (B \imp A)) \imp (B \iff A)) in F by A2, Def38;

then A3: ((A \imp B) \and (B \imp A)) \imp (B \iff A) in F by A1, Def38;

A4: ((A \iff B) \imp (A \imp B)) \imp (((A \iff B) \imp (B \imp A)) \imp ((A \iff B) \imp ((A \imp B) \and (B \imp A)))) in F by Th49;

A5: ( (A \iff B) \imp (A \imp B) in F & (A \iff B) \imp (B \imp A) in F ) by Def38;

then ((A \iff B) \imp (B \imp A)) \imp ((A \iff B) \imp ((A \imp B) \and (B \imp A))) in F by A4, Def38;

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

((A \iff B) \imp ((A \imp B) \and (B \imp A))) \imp ((((A \imp B) \and (B \imp A)) \imp (B \iff A)) \imp ((A \iff B) \imp (B \iff A))) in F by Th39;

then (((A \imp B) \and (B \imp A)) \imp (B \iff A)) \imp ((A \iff B) \imp (B \iff A)) in F by A6, Def38;

hence (A \iff B) \imp (B \iff A) in F by A3, Def38; :: thesis: verum

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 (B \iff A) 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 (B \iff A) 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 (B \iff A) in F

let F be PC-theory of L; :: thesis: for A, B being Formula of L holds (A \iff B) \imp (B \iff A) in F

let A, B be Formula of L; :: thesis: (A \iff B) \imp (B \iff A) in F

A1: ((B \imp A) \and (A \imp B)) \imp (B \iff A) in F by Def38;

A2: ((A \imp B) \and (B \imp A)) \imp ((B \imp A) \and (A \imp B)) in F by Th50;

(((A \imp B) \and (B \imp A)) \imp ((B \imp A) \and (A \imp B))) \imp ((((B \imp A) \and (A \imp B)) \imp (B \iff A)) \imp (((A \imp B) \and (B \imp A)) \imp (B \iff A))) in F by Th39;

then (((B \imp A) \and (A \imp B)) \imp (B \iff A)) \imp (((A \imp B) \and (B \imp A)) \imp (B \iff A)) in F by A2, Def38;

then A3: ((A \imp B) \and (B \imp A)) \imp (B \iff A) in F by A1, Def38;

A4: ((A \iff B) \imp (A \imp B)) \imp (((A \iff B) \imp (B \imp A)) \imp ((A \iff B) \imp ((A \imp B) \and (B \imp A)))) in F by Th49;

A5: ( (A \iff B) \imp (A \imp B) in F & (A \iff B) \imp (B \imp A) in F ) by Def38;

then ((A \iff B) \imp (B \imp A)) \imp ((A \iff B) \imp ((A \imp B) \and (B \imp A))) in F by A4, Def38;

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

((A \iff B) \imp ((A \imp B) \and (B \imp A))) \imp ((((A \imp B) \and (B \imp A)) \imp (B \iff A)) \imp ((A \iff B) \imp (B \iff A))) in F by Th39;

then (((A \imp B) \and (B \imp A)) \imp (B \iff A)) \imp ((A \iff B) \imp (B \iff A)) in F by A6, Def38;

hence (A \iff B) \imp (B \iff A) in F by A3, Def38; :: thesis: verum