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' p1 |-| 'not' q1 ) )
assume that
A1: p1 is_an_universal_closure_of p and
A2: q1 is_an_universal_closure_of q ; :: thesis: ( p |-| q iff 'not' p1 |-| 'not' q1 )

now

assume A3: p |-| q ; :: thesis: 'not' p1 |-| 'not' q1
then q |- p by Def5;
then A4: 'not' p1 |- 'not' q1 by A1, A2, Th48;
p |- q by A3, Def5;
then 'not' q1 |- 'not' p1 by A1, A2, Th48;
hence 'not' p1 |-| 'not' q1 by A4, Def5; :: thesis: verum

end;

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

now

assume A5: 'not' p1 |-| 'not' q1 ; :: thesis: p |-| q
then 'not' p1 |- 'not' q1 by Def5;
then A6: q |- p by A1, A2, Th48;
'not' q1 |- 'not' p1 by A5, Def5;
then p |- q by A1, A2, Th48;
hence p |-| q by A6, Def5; :: thesis: verum

end;

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