theorem :: CQC_THE3:49

for A being QC-alphabet
for p, q, p1, q1 being Element of CQC-WFF A st p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q holds
( p |-| q iff 'not' p1 |-| 'not' q1 ) by Th48;