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 being Formula of L holds \not (A \and (\not 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 being Formula of L holds \not (A \and (\not A)) in F
let L be language MSAlgebra over S; :: thesis: for F being PC-theory of L
for A being Formula of L holds \not (A \and (\not A)) in F
let F be PC-theory of L; :: thesis: for A being Formula of L holds \not (A \and (\not A)) in F
let A be Formula of L; :: thesis: \not (A \and (\not A)) in F
( (\not A) \imp (\not A) in F & A \imp (\not (\not A)) in F ) by Th34, Th64;
then ( ((\not A) \and A) \imp ((\not A) \and (\not (\not A))) in F & ((\not A) \and (\not (\not A))) \imp (\not (A \or (\not A))) in F ) by Th74, Th72;
then ((\not A) \and A) \imp (\not (A \or (\not A))) in F by Th45;
then ( (\not (\not (A \or (\not A)))) \imp (\not ((\not A) \and A)) in F & (A \or (\not A)) \imp (\not (\not (A \or (\not A)))) in F ) by Th64, Th58;
then ( (A \or (\not A)) \imp (\not ((\not A) \and A)) in F & A \or (\not A) in F ) by Th45, Def38;
then A1: \not ((\not A) \and A) in F by Def38;
(A \and (\not A)) \imp ((\not A) \and A) in F by Th50;
then (\not ((\not A) \and A)) \imp (\not (A \and (\not A))) in F by Th58;
hence \not (A \and (\not A)) in F by Def38, A1; :: thesis: verum