let p, q be Element of CQC-WFF ; :: thesis: ( p is negative & q = the_argument_of p implies SepVar p = 'not' (SepVar q) )
assume ( p is negative & q = the_argument_of p ) ; :: thesis: SepVar p = 'not' (SepVar q)
then p = 'not' q by QC_LANG1:def 23;
hence SepVar p = 'not' (SepVar q) by Th29; :: thesis: verum