:: deftheorem Def38 defines PC-closed AOFA_L00:def 42 :
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 Subset of ( the Sorts of L . the formula-sort of S) holds
( F is PC-closed iff for A, B, C being Formula of L holds
( A \imp (B \imp A) in F & (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) in F & ((\not A) \imp (\not B)) \imp (B \imp A) in F & A \imp (A \or B) in F & A \imp (B \or A) in F & (A \imp C) \imp ((B \imp C) \imp ((A \or B) \imp C)) in F & (A \and B) \imp A in F & (A \and B) \imp B in F & A \imp (B \imp (A \and B)) in F & (A \and (\not A)) \imp B in F & (A \imp B) \imp ((A \imp (\not B)) \imp (\not A)) in F & A \or (\not A) in F & (A \iff B) \imp (A \imp B) in F & (A \iff B) \imp (B \imp A) in F & ((A \imp B) \and (B \imp A)) \imp (A \iff B) in F & \true_ L in F & ((\true_ L) \and A) \iff A in F & ((\true_ L) \or A) \iff (\true_ L) in F & ( A in F & A \imp B in F implies B in F ) ) );