theorem Th58: :: AOFA_L00:60

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