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

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

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

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

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

( (C \and (\not C)) \imp B in F & ((\not C) \and C) \imp (C \and (\not C)) in F ) by Th50, Def38;

then ( ((\not C) \and C) \imp B in F & B \imp B in F ) by Th34, Th45;

then ( (B \or ((\not C) \and C)) \imp (B \or B) in F & (B \or B) \imp B in F ) by Th59, Th52;

hence (B \or ((\not C) \and C)) \imp B in F by Th45; :: thesis: verum

for L being language MSAlgebra over S

for F being PC-theory of L

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

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

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

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

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

( (C \and (\not C)) \imp B in F & ((\not C) \and C) \imp (C \and (\not C)) in F ) by Th50, Def38;

then ( ((\not C) \and C) \imp B in F & B \imp B in F ) by Th34, Th45;

then ( (B \or ((\not C) \and C)) \imp (B \or B) in F & (B \or B) \imp B in F ) by Th59, Th52;

hence (B \or ((\not C) \and C)) \imp B in F by Th45; :: thesis: verum