theorem Th48: :: CQC_THE3:48

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' q1 |- 'not' p1 )