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, C being Formula of L holds (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) 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, C being Formula of L holds (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) in F

let L be language MSAlgebra over S; :: thesis: for F being PC-theory of L

for A, B, C being Formula of L holds (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) in F

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

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

set AB = A \or B;

set AC = A \or C;

set BC = B \and C;

set ABC = A \or (B \and C);

A1: ((A \or (B \and C)) \imp (A \or B)) \imp (((A \or (B \and C)) \imp (A \or C)) \imp ((A \or (B \and C)) \imp ((A \or B) \and (A \or C)))) in F by Th49;

A2: (A \imp (A \or B)) \imp (((B \and C) \imp (A \or B)) \imp ((A \or (B \and C)) \imp (A \or B))) in F by Def38;

A3: (A \imp (A \or C)) \imp (((B \and C) \imp (A \or C)) \imp ((A \or (B \and C)) \imp (A \or C))) in F by Def38;

A4: ( A \imp (A \or C) in F & A \imp (A \or B) in F ) by Def38;

( (B \and C) \imp C in F & (B \and C) \imp B in F & B \imp (A \or B) in F & C \imp (A \or C) in F ) by Def38;

then A5: ( (B \and C) \imp (A \or B) in F & (B \and C) \imp (A \or C) in F ) by Th45;

( ((B \and C) \imp (A \or B)) \imp ((A \or (B \and C)) \imp (A \or B)) in F & ((B \and C) \imp (A \or C)) \imp ((A \or (B \and C)) \imp (A \or C)) in F ) by A2, A3, A4, Def38;

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

then ((A \or (B \and C)) \imp (A \or C)) \imp ((A \or (B \and C)) \imp ((A \or B) \and (A \or C))) in F by A1, Def38;

hence (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) in F by A6, Def38; :: thesis: verum

for L being language MSAlgebra over S

for F being PC-theory of L

for A, B, C being Formula of L holds (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) 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, C being Formula of L holds (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) in F

let L be language MSAlgebra over S; :: thesis: for F being PC-theory of L

for A, B, C being Formula of L holds (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) in F

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

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

set AB = A \or B;

set AC = A \or C;

set BC = B \and C;

set ABC = A \or (B \and C);

A1: ((A \or (B \and C)) \imp (A \or B)) \imp (((A \or (B \and C)) \imp (A \or C)) \imp ((A \or (B \and C)) \imp ((A \or B) \and (A \or C)))) in F by Th49;

A2: (A \imp (A \or B)) \imp (((B \and C) \imp (A \or B)) \imp ((A \or (B \and C)) \imp (A \or B))) in F by Def38;

A3: (A \imp (A \or C)) \imp (((B \and C) \imp (A \or C)) \imp ((A \or (B \and C)) \imp (A \or C))) in F by Def38;

A4: ( A \imp (A \or C) in F & A \imp (A \or B) in F ) by Def38;

( (B \and C) \imp C in F & (B \and C) \imp B in F & B \imp (A \or B) in F & C \imp (A \or C) in F ) by Def38;

then A5: ( (B \and C) \imp (A \or B) in F & (B \and C) \imp (A \or C) in F ) by Th45;

( ((B \and C) \imp (A \or B)) \imp ((A \or (B \and C)) \imp (A \or B)) in F & ((B \and C) \imp (A \or C)) \imp ((A \or (B \and C)) \imp (A \or C)) in F ) by A2, A3, A4, Def38;

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

then ((A \or (B \and C)) \imp (A \or C)) \imp ((A \or (B \and C)) \imp ((A \or B) \and (A \or C))) in F by A1, Def38;

hence (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) in F by A6, Def38; :: thesis: verum