theorem Th100: :: AOFA_L00:102

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 A, B, C, D being Formula of L st A \iff (B \or C) in F & B \iff D in F holds
A \iff (D \or C) in F