theorem Th84: :: AOFA_L00:86

for n being non empty Nat
for S being non empty non void b₁ 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