let A be QC-alphabet ; :: thesis: 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 )
let p, q, p1, q1 be Element of CQC-WFF A; :: 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 :: thesis: ( p |- q implies 'not' q1 |- 'not' p1 )
q |-| q1 by A2, Th38;
then A3: q |- q1 ;
p1 |-| p by A1, Th38;
then A4: p1 |- p ;
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;
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 :: thesis: ( 'not' q1 |- 'not' p1 implies p |- q )
q1 |-| q by A2, Th38;
then A6: q1 |- q ;
p1 |-| p by A1, Th38;
then A7: p |- p1 ;
assume A8: 'not' q1 |- 'not' p1 ; :: thesis: p |- q
q1 is closed by A2;
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