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