theorem Th76: :: AOFA_L00:78

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) \or C) \iff (A \or (B \or C)) in F