let p1, p, q1, q be Element of CQC-WFF ; :: thesis: ( p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies ( p |- q iff 'not' q1 |- 'not' p1 ) )
assume that
A1: p1 is_an_universal_closure_of p and
A2: q1 is_an_universal_closure_of q ; :: thesis: ( p |- q iff 'not' q1 |- 'not' p1 )

now

q |-| q1 by A2, Th38;
then A3: q |- q1 by Def5;
p1 |-| p by A1, Th38;
then A4: p1 |- p by Def5;
assume p |- q ; :: thesis: 'not' q1 |- 'not' p1
then p1 |- q by A4, Th6;
then A5: p1 |- q1 by A3, Th6;
p1 is closed by A1, Def6;
hence 'not' q1 |- 'not' p1 by A5, Th43; :: thesis: verum

end;

hence ( p |- q implies 'not' q1 |- 'not' p1 ) ; :: thesis: ( 'not' q1 |- 'not' p1 implies p |- q )

now

q1 |-| q by A2, Th38;
then A6: q1 |- q by Def5;
p1 |-| p by A1, Th38;
then A7: p |- p1 by Def5;
assume A8: 'not' q1 |- 'not' p1 ; :: thesis: p |- q
q1 is closed by A2, Def6;
then p1 |- q1 by A8, Th45;
then p |- q1 by A7, Th6;
hence p |- q by A6, Th6; :: thesis: verum

end;

hence ( 'not' q1 |- 'not' p1 implies p |- q ) ; :: thesis: verum