let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p is negative & q = the_argument_of p holds
SepVar p = 'not' (SepVar q)
let p, q be Element of CQC-WFF A; :: 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 24;
hence SepVar p = 'not' (SepVar q) by Th28; :: thesis: verum