theorem :: AOFA_L00:57

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 being Formula of L holds (A \or (B \and C)) \imp ((A \or B) \and (A \or C)) in F