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 \and B) \or (A \and C)) \imp (A \and (B \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 \and B) \or (A \and C)) \imp (A \and (B \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 \and B) \or (A \and C)) \imp (A \and (B \or C)) in F

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

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

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

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

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

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

set AB = A \and B;

set AC = A \and C;

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

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

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

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

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

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

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

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

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

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

hence ((A \and B) \or (A \and C)) \imp (A \and (B \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 \and B) \or (A \and C)) \imp (A \and (B \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 \and B) \or (A \and C)) \imp (A \and (B \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 \and B) \or (A \and C)) \imp (A \and (B \or C)) in F

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

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

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

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

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

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

set AB = A \and B;

set AC = A \and C;

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

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

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

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

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

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

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

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

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

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

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