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