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

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