let n be non empty Nat; 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 being Formula of L holds (A \imp B) \imp ((\not A) \or B) in F
let S be 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 being Formula of L holds (A \imp B) \imp ((\not A) \or B) in F
let L be language MSAlgebra over S; for F being PC-theory of L
for A, B being Formula of L holds (A \imp B) \imp ((\not A) \or B) in F
let F be PC-theory of L; for A, B being Formula of L holds (A \imp B) \imp ((\not A) \or B) in F
let A, B be Formula of L; (A \imp B) \imp ((\not A) \or B) in F
A1:
(A \imp B) \imp (A \imp B) in F
by Th34;
((A \imp B) \imp (A \imp B)) \imp (((A \imp B) \and A) \imp B) in F
by Th48;
then
( ((A \imp B) \and A) \imp B in F & (\not A) \imp (\not A) in F )
by A1, Def38, Th34;
then A2:
((\not A) \or ((A \imp B) \and A)) \imp ((\not A) \or B) in F
by Th59;
(((\not A) \or (A \imp B)) \and ((\not A) \or A)) \imp ((\not A) \or ((A \imp B) \and A)) in F
by Th80;
then A3:
(((\not A) \or (A \imp B)) \and ((\not A) \or A)) \imp ((\not A) \or B) in F
by A2, Th45;
(((\not A) \or A) \and ((\not A) \or (A \imp B))) \imp (((\not A) \or (A \imp B)) \and ((\not A) \or A)) in F
by Th50;
then A4:
(((\not A) \or A) \and ((\not A) \or (A \imp B))) \imp ((\not A) \or B) in F
by A3, Th45;
((((\not A) \or A) \and ((\not A) \or (A \imp B))) \imp ((\not A) \or B)) \imp (((\not A) \or A) \imp (((\not A) \or (A \imp B)) \imp ((\not A) \or B))) in F
by Th47;
then A5:
((\not A) \or A) \imp (((\not A) \or (A \imp B)) \imp ((\not A) \or B)) in F
by A4, Def38;
( A \or (\not A) in F & (A \or (\not A)) \imp ((\not A) \or A) in F )
by Def38, Th36;
then
(\not A) \or A in F
by Def38;
then A6:
((\not A) \or (A \imp B)) \imp ((\not A) \or B) in F
by A5, Def38;
(A \imp B) \imp ((\not A) \or (A \imp B)) in F
by Def38;
hence
(A \imp B) \imp ((\not A) \or B) in F
by A6, Th45; verum